Theorem 19.8a 1464

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		id 19	. . 3 ⊢ (∃xφ → ∃xφ)
2		hbe1 1365	. . . 4 ⊢ (∃xφ → ∀x∃xφ)
3	2	19.23h 1368	. . 3 ⊢ (∀x(φ → ∃xφ) ↔ (∃xφ → ∃xφ))
4	1, 3	mpbir 134	. 2 ⊢ ∀x(φ → ∃xφ)
5	4	spi 1411	1 ⊢ (φ → ∃xφ)

Syntax hints:   → wi 4  ∀wal 1226  ∃wex 1362

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  19.23bi  1465  exim  1472  19.43  1501  hbex  1509  19.2  1511  19.9t  1515  19.9h  1516  excomim  1535  19.38  1548  nexr  1564  sbequ1  1633  equs5e  1658  exdistrfor  1663  sbcof2  1673  mo2n  1910  euor2  1940  2moex  1968  2euex  1969  2moswapdc  1972  2exeu  1974  rspe  2348  rsp2e  2350  ceqex  2648  vn0m  3209  intab  3618  copsexg  3955  eusv2nf  4138  dmcosseq  4530  dminss  4665  imainss  4666  relssdmrn  4768  oprabid  5461  tfrlemibxssdm  5862  ltsopr  6433  ltexprlemm  6437  recexprlemopl  6459  recexprlemopu  6461