Theorem 19.8a 1795

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.) Revised in conjunction with a shortening of sp 1796. (Revised by Wolf Lammen, 13-Jan-2018.)

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 1712	. 2 |- E. w w = x
2		ax-5 1671	. . . . 5 |- ( ph -> A. w ph )
3		ax-12 1794	. . . . 5 |- ( x = w -> ( A. w ph -> A. x ( x = w -> ph ) ) )
4		ax6ev 1712	. . . . . 6 |- E. x x = w
5		exim 1624	. . . . . 6 |- ( A. x ( x = w -> ph ) -> ( E. x x = w -> E. x ph ) )
6	4, 5	mpi 17	. . . . 5 |- ( A. x ( x = w -> ph ) -> E. x ph )
7	2, 3, 6	syl56 34	. . . 4 |- ( x = w -> ( ph -> E. x ph ) )
8	7	equcoms 1735	. . 3 |- ( w = x -> ( ph -> E. x ph ) )
9	8	exlimiv 1689	. 2 |- ( E. w w = x -> ( ph -> E. x ph ) )
10	1, 9	ax-mp 5	1 |- ( ph -> E. x ph )

Syntax hints:   -> wi 4   A.wal 1368   E.wex 1587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

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

This theorem is referenced by:  sp  1796  19.2g  1805  19.23bi  1807  nexr  1808  19.9t  1826  nfdiOLD  1900  qexmid  1914  sbequ1  1944  ax6e  1955  exdistrf  2032  equvini  2044  2ax6e  2165  ax12indn  2251  mo2vOLD  2268  mo2vOLDOLD  2269  moOLD  2312  euor2  2319  euor2OLD  2320  mo2OLD  2321  2moex  2359  2euex  2360  2moswap  2363  2mo  2367  2moOLD  2368  2moOLDOLD  2369  rspe  2887  rsp2e  2889  ceqex  3189  mo2icl  3237  intab  4258  eusv2nf  4590  copsexg  4676  copsexgOLD  4677  dmcosseq  5201  dminss  5351  imainss  5352  relssdmrn  5458  oprabid  6216  hta  8207  domtriomlem  8714  axextnd  8858  axrepnd  8861  axunndlem1  8862  axunnd  8863  axpowndlem2  8865  axpowndlem2OLD  8866  axpownd  8870  axregndlem1  8871  axregnd  8873  axregndOLD  8874  axacndlem1  8877  axacndlem2  8878  axacndlem3  8879  axacndlem4  8880  axacndlem5  8881  axacnd  8882  fpwwe  8916  pwfseqlem4a  8931  pwfseqlem4  8932  reclem2pr  9320  amosym1  28408  wl-exeq  28503  finminlem  28653  pm11.58  29783  axc11next  29800  iotavalsb  29827  19.8ad  31350  vk15.4j  31535  onfrALTlem1  31558  onfrALTlem1VD  31928  vk15.4jVD  31952  bnj1121  32278  bnj1189  32302  bj-19.23bit  32482  bj-nexrt  32483  bj-19.9htbi  32495  bj-finsumval0  32891