Theorem genex-P6 731

Description: The WFF '∃𝑥𝜑' is General For '𝑥'.

See genexw-P6 677 for a version that requires only FOL axioms.

Assertion

Ref	Expression
genex-P6	⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)

Proof of Theorem genex-P6

Step	Hyp	Ref	Expression
1		gennall-P6 730	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑)
2		df-exists-D5.1 596	. . . 4 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
3	2	bisym-P3.33b.RC 299	. . 3 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ∃𝑥𝜑)
4	3	suballinf-P5 594	. . 3 ⊢ (∀𝑥 ¬ ∀𝑥 ¬ 𝜑 ↔ ∀𝑥∃𝑥𝜑)
5	3, 4	subimd-P3.40c.RC 330	. 2 ⊢ ((¬ ∀𝑥 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑) ↔ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑))
6	1, 5	bimpf-P4.RC 532	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-L10 27

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-true-D2.4 155  df-exists-D5.1 596

This theorem is referenced by:  nfrex1-P6  742