Theorem 19.8a 1756

Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
19.8a	⊢ (φ → ∃xφ)

Proof of Theorem 19.8a

Step	Hyp	Ref	Expression
1		sp 1747	. . 3 ⊢ (∀x ¬ φ → ¬ φ)
2	1	con2i 112	. 2 ⊢ (φ → ¬ ∀x ¬ φ)
3		df-ex 1542	. 2 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
4	2, 3	sylibr 203	1 ⊢ (φ → ∃xφ)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  19.2g  1757  19.23bi  1759  nexr  1760  19.9t  1779  19.9hOLD  1781  19.23tOLD  1819  19.23hOLD  1820  19.9tOLD  1857  excomimOLD  1858  19.38OLD  1874  qexmid  1886  sbequ1  1918  ax12olem5  1931  ax10lem2  1937  exdistrf  1971  ax11indn  2195  mo  2226  mo2  2233  euor2  2272  2moex  2275  2euex  2276  2moswap  2279  2mo  2282  rspe  2676  rsp2e  2678  ceqex  2970  mo2icl  3016  necompl  3545  intab  3957  copsexg  4608  imainss  5043  nfunv  5139  oprabid  5551