Theorem 19.8a 1801

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, 9-Jan-1993.) Allow a shortening of sp 1803. (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 1716	. 2 |- E. w w = x
2		ax12v 1799	. . . . 5 |- ( x = w -> ( ph -> A. x ( x = w -> ph ) ) )
3		ax6ev 1716	. . . . . 6 |- E. x x = w
4		exim 1628	. . . . . 6 |- ( A. x ( x = w -> ph ) -> ( E. x x = w -> E. x ph ) )
5	3, 4	mpi 17	. . . . 5 |- ( A. x ( x = w -> ph ) -> E. x ph )
6	2, 5	syl6 33	. . . 4 |- ( x = w -> ( ph -> E. x ph ) )
7	6	equcoms 1739	. . 3 |- ( w = x -> ( ph -> E. x ph ) )
8	7	exlimiv 1693	. 2 |- ( E. w w = x -> ( ph -> E. x ph ) )
9	1, 8	ax-mp 5	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1372   E.wex 1591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798

This theorem depends on definitions:  df-bi 185  df-ex 1592

This theorem is referenced by:  sp  1803  19.2g  1812  19.23bi  1814  nexr  1815  19.9t  1833  nfdiOLD  1907  qexmid  1921  sbequ1  1953  ax6e  1964  exdistrf  2041  equvini  2053  2ax6e  2173  ax12indn  2259  mo2vOLD  2276  mo2vOLDOLD  2277  moOLD  2320  euor2  2327  euor2OLD  2328  mo2OLD  2329  2moex  2367  2euex  2368  2moswap  2371  2mo  2375  2moOLD  2376  2moOLDOLD  2377  rspe  2915  rsp2eOLD  2917  ceqex  3227  mo2icl  3275  intab  4305  eusv2nf  4638  copsexg  4725  copsexgOLD  4726  dmcosseq  5255  dminss  5411  imainss  5412  relssdmrn  5519  oprabid  6299  hta  8304  domtriomlem  8811  axextnd  8955  axrepnd  8958  axunndlem1  8959  axunnd  8960  axpowndlem2  8962  axpowndlem2OLD  8963  axpownd  8967  axregndlem1  8968  axregnd  8970  axregndOLD  8971  axacndlem1  8974  axacndlem2  8975  axacndlem3  8976  axacndlem4  8977  axacndlem5  8978  axacnd  8979  fpwwe  9013  pwfseqlem4a  9028  pwfseqlem4  9029  reclem2pr  9415  amosym1  29318  wl-exeq  29414  finminlem  29564  pm11.58  30693  axc11next  30710  iotavalsb  30737  suprnmpt  30848  ssfiunibd  30905  19.8ad  32067  vk15.4j  32252  onfrALTlem1  32275  onfrALTlem1VD  32645  vk15.4jVD  32669  bnj1121  32995  bnj1189  33019  bj-19.23bit  33201  bj-nexrt  33202  bj-19.9htbi  33214  bj-finsumval0  33610