Theorem 19.8a 1912

Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. See 19.8v 1804 for a version requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1914. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)

Assertion

Ref	Expression
19.8a	|- ( ph -> E. x ph )

Proof of Theorem 19.8a

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax6ev 1800	. 2 |- E. w w = x
2		ax12v 1910	. . . . 5 |- ( x = w -> ( ph -> A. x ( x = w -> ph ) ) )
3		ax6ev 1800	. . . . 5 |- E. x x = w
4		exim 1700	. . . . 5 |- ( A. x ( x = w -> ph ) -> ( E. x x = w -> E. x ph ) )
5	2, 3, 4	syl6mpi 64	. . . 4 |- ( x = w -> ( ph -> E. x ph ) )
6	5	equcoms 1849	. . 3 |- ( w = x -> ( ph -> E. x ph ) )
7	6	exlimiv 1770	. 2 |- ( E. w w = x -> ( ph -> E. x ph ) )
8	1, 7	ax-mp 5	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1435   E.wex 1657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909

This theorem depends on definitions:  df-bi 188  df-ex 1658

This theorem is referenced by:  sp  1914  19.2g  1923  19.23bi  1926  nexr  1927  19.9t  1946  19.9tOLD  1949  qexmid  2036  sbequ1  2050  ax6e  2060  exdistrf  2134  equvini  2146  2ax6e  2249  euor2  2313  2moex  2342  2euex  2343  2moswap  2346  2mo  2350  rspe  2880  rsp2eOLD  2882  ceqex  3201  mo2icl  3249  intab  4286  eusv2nf  4622  copsexg  4706  dmcosseq  5115  dminss  5269  imainss  5270  relssdmrn  5375  oprabid  6333  hta  8377  domtriomlem  8880  axextnd  9024  axrepnd  9027  axunndlem1  9028  axunnd  9029  axpowndlem2  9031  axpownd  9034  axregndlem1  9035  axregnd  9037  axacndlem1  9040  axacndlem2  9041  axacndlem3  9042  axacndlem4  9043  axacndlem5  9044  axacnd  9045  fpwwe  9079  pwfseqlem4a  9094  pwfseqlem4  9095  reclem2pr  9481  bnj1121  29803  bnj1189  29827  finminlem  30980  amosym1  31092  bj-19.23bit  31245  bj-nexrt  31246  bj-19.9htbi  31258  bj-nfdiOLD  31415  bj-finsumval0  31667  isbasisrelowllem1  31723  isbasisrelowllem2  31724  wl-exeq  31832  ax12indn  32484  pm11.58  36711  axc11next  36728  iotavalsb  36755  vk15.4j  36856  onfrALTlem1  36885  onfrALTlem1VD  37261  vk15.4jVD  37285  suprnmpt  37400  ssfiunibd  37482  ovncvrrp  38291  19.8ad  40088