Theorem 19.8a 1910

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 1803 for a version requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1912. (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 1799	. 2 |- E. w w = x
2		ax12v 1908	. . . . 5 |- ( x = w -> ( ph -> A. x ( x = w -> ph ) ) )
3		ax6ev 1799	. . . . 5 |- E. x x = w
4		exim 1701	. . . . 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 1847	. . 3 |- ( w = x -> ( ph -> E. x ph ) )
7	6	exlimiv 1769	. 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 1659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907

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

This theorem is referenced by:  sp  1912  19.2g  1921  19.23bi  1924  nexr  1925  19.9t  1944  19.9tOLD  1947  qexmid  2034  sbequ1  2048  ax6e  2058  exdistrf  2131  equvini  2143  2ax6e  2246  mo2vOLD  2274  mo2vOLDOLD  2275  euor2  2313  2moex  2343  2euex  2344  2moswap  2347  2mo  2351  2moOLD  2352  rspe  2890  rsp2eOLD  2892  ceqex  3208  mo2icl  3256  intab  4289  eusv2nf  4623  copsexg  4707  dmcosseq  5116  dminss  5270  imainss  5271  relssdmrn  5376  oprabid  6332  hta  8367  domtriomlem  8870  axextnd  9014  axrepnd  9017  axunndlem1  9018  axunnd  9019  axpowndlem2  9021  axpownd  9024  axregndlem1  9025  axregnd  9027  axregndOLD  9028  axacndlem1  9031  axacndlem2  9032  axacndlem3  9033  axacndlem4  9034  axacndlem5  9035  axacnd  9036  fpwwe  9070  pwfseqlem4a  9085  pwfseqlem4  9086  reclem2pr  9472  bnj1121  29582  bnj1189  29606  finminlem  30759  amosym1  30871  bj-19.23bit  31024  bj-nexrt  31025  bj-19.9htbi  31037  bj-nfdiOLD  31195  bj-finsumval0  31447  isbasisrelowllem1  31492  isbasisrelowllem2  31493  wl-exeq  31574  ax12indn  32223  pm11.58  36377  axc11next  36394  iotavalsb  36421  vk15.4j  36522  onfrALTlem1  36551  onfrALTlem1VD  36927  vk15.4jVD  36951  suprnmpt  37061  ssfiunibd  37136  19.8ad  39207