Theorem 19.8a 1479

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 1381	. . . 4 ⊢ (∃xφ → ∀x∃xφ)
3	2	19.23h 1384	. . 3 ⊢ (∀x(φ → ∃xφ) ↔ (∃xφ → ∃xφ))
4	1, 3	mpbir 134	. 2 ⊢ ∀x(φ → ∃xφ)
5	4	spi 1426	1 ⊢ (φ → ∃xφ)

Syntax hints:   → wi 4  ∀wal 1240  ∃wex 1378

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 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  19.23bi  1480  exim  1487  19.43  1516  hbex  1524  19.2  1526  19.9t  1530  19.9h  1531  excomim  1550  19.38  1563  nexr  1579  sbequ1  1648  equs5e  1673  exdistrfor  1678  sbcof2  1688  mo2n  1925  euor2  1955  2moex  1983  2euex  1984  2moswapdc  1987  2exeu  1989  rspe  2364  rsp2e  2366  ceqex  2665  vn0m  3226  intab  3635  copsexg  3972  eusv2nf  4154  dmcosseq  4546  dminss  4681  imainss  4682  relssdmrn  4784  oprabid  5480  tfrlemibxssdm  5882  nqprl  6533  ltsopr  6570  ltexprlemm  6574  recexprlemopl  6597  recexprlemopu  6599