Theorem spec-P6 719

Description: Law of Specialization.

See specw-P5 661 for a version that requires only FOL axioms.

Assertion

Ref	Expression
spec-P6	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem spec-P6

Step	Hyp	Ref	Expression
1		exi-P6 718	. . 3 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
2	1	trnsp-P3.31b.RC 283	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 → 𝜑)
3		allasex-P5 599	. . 3 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
4	3	bisym-P3.33b.RC 299	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜑 ↔ ∀𝑥𝜑)
5	2, 4	subiml2-P4.RC 541	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ∀wff-forall 8  ¬ wff-neg 9   → wff-imp 10  ∃wff-exists 595

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596

This theorem is referenced by:  qremall-P6  722  qremex-P6  723  lemma-L6.01a  724  nfrterm-P6  779  qremexd-P6  823