Theorem hbe1 709

Description: x is not free in ∃xφ.

Assertion

Ref	Expression
hbe1	⊢ (∃xφ → ∀x∃xφ)

Proof of Theorem hbe1

Step	Hyp	Ref	Expression
1		hbn1 708	. 2 ⊢ (¬ ∀x ¬ φ → ∀x ¬ ∀x ¬ φ)
2		df-ex 679	. 2 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
3	2	bial 695	. 2 ⊢ (∀x∃xφ ↔ ∀x ¬ ∀x ¬ φ)
4	1, 2, 3	3imtr4 192	1 ⊢ (∃xφ → ∀x∃xφ)

Syntax hints:  ¬ wn 1   → wi 2  ∀wal 672  ∃wex 678

This theorem is referenced by:  excomim 727  19.23 745  19.38 760  exan 784  hbmo1 1032  mopick2 1057  moexex 1058  2moex 1060  2euex 1061  2moswap 1064  2exeu 1066  2eu4 1070  hbre1 1239  ceqsexg 1411  axrep 1473  axrep2 1474  zfrep2 1475  copsex2g 1903  mosubop 1911  hbopab1 2112  hbopab2 2113  dmcosseq 2572  imadif 2714  hboprab1 3023  hboprab2 3024  zfcndrep 3760  zfcndpow 3762  zfcndreg 3763  zfcndinf 3764  suppsr3 4018

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org