Theorem 19.8a 1862

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 1758 for a version requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1864. (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 1754	. 2 |- E. w w = x
2		ax12v 1860	. . . . 5 |- ( x = w -> ( ph -> A. x ( x = w -> ph ) ) )
3		ax6ev 1754	. . . . 5 |- E. x x = w
4		exim 1659	. . . . 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 1800	. . 3 |- ( w = x -> ( ph -> E. x ph ) )
7	6	exlimiv 1727	. 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 1396   E.wex 1617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859

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

This theorem is referenced by:  sp  1864  19.2g  1873  19.23bi  1876  nexr  1877  19.9t  1895  nfdiOLD  1968  qexmid  1982  sbequ1  1996  ax6e  2007  exdistrf  2079  equvini  2091  2ax6e  2196  ax12indn  2275  mo2vOLD  2292  mo2vOLDOLD  2293  euor2  2332  2moex  2362  2euex  2363  2moswap  2366  2mo  2370  2moOLD  2371  rspe  2912  rsp2eOLD  2914  ceqex  3227  mo2icl  3275  intab  4302  eusv2nf  4635  copsexg  4722  dmcosseq  5253  dminss  5405  imainss  5406  relssdmrn  5511  oprabid  6297  hta  8306  domtriomlem  8813  axextnd  8957  axrepnd  8960  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  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  30119  wl-exeq  30227  finminlem  30376  pm11.58  31537  axc11next  31554  iotavalsb  31581  suprnmpt  31691  ssfiunibd  31748  19.8ad  33501  vk15.4j  33685  onfrALTlem1  33714  onfrALTlem1VD  34091  vk15.4jVD  34115  bnj1121  34442  bnj1189  34466  bj-19.23bit  34645  bj-nexrt  34646  bj-19.9htbi  34658  bj-finsumval0  35063