Theorem 19.8a 1841

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 1738 for a version requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1843. (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 1734	. 2 |- E. w w = x
2		ax12v 1839	. . . . 5 |- ( x = w -> ( ph -> A. x ( x = w -> ph ) ) )
3		ax6ev 1734	. . . . 5 |- E. x x = w
4		exim 1639	. . . . 5 |- ( A. x ( x = w -> ph ) -> ( E. x x = w -> E. x ph ) )
5	2, 3, 4	syl6mpi 62	. . . 4 |- ( x = w -> ( ph -> E. x ph ) )
6	5	equcoms 1779	. . 3 |- ( w = x -> ( ph -> E. x ph ) )
7	6	exlimiv 1707	. 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 1379   E.wex 1597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838

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

This theorem is referenced by:  sp  1843  19.2g  1852  19.23bi  1855  nexr  1856  19.9t  1874  nfdiOLD  1947  qexmid  1961  sbequ1  1975  ax6e  1986  exdistrf  2059  equvini  2071  2ax6e  2178  ax12indn  2257  mo2vOLD  2274  mo2vOLDOLD  2275  euor2  2317  mo2OLD  2318  2moex  2349  2euex  2350  2moswap  2353  2mo  2357  2moOLD  2358  rspe  2899  rsp2eOLD  2901  ceqex  3214  mo2icl  3262  intab  4298  eusv2nf  4631  copsexg  4718  copsexgOLD  4719  dmcosseq  5250  dminss  5406  imainss  5407  relssdmrn  5514  oprabid  6304  hta  8313  domtriomlem  8820  axextnd  8964  axrepnd  8967  axunndlem1  8968  axunnd  8969  axpowndlem2  8971  axpowndlem2OLD  8972  axpownd  8976  axregndlem1  8977  axregnd  8979  axregndOLD  8980  axacndlem1  8983  axacndlem2  8984  axacndlem3  8985  axacndlem4  8986  axacndlem5  8987  axacnd  8988  fpwwe  9022  pwfseqlem4a  9037  pwfseqlem4  9038  reclem2pr  9424  amosym1  29859  wl-exeq  29955  finminlem  30104  pm11.58  31243  axc11next  31260  iotavalsb  31287  suprnmpt  31397  ssfiunibd  31454  19.8ad  32821  vk15.4j  33006  onfrALTlem1  33028  onfrALTlem1VD  33398  vk15.4jVD  33422  bnj1121  33748  bnj1189  33772  bj-19.23bit  33958  bj-nexrt  33959  bj-19.9htbi  33971  bj-finsumval0  34365