Theorem spcev 3511

Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypotheses

Ref	Expression
spcv.1	⊢ 𝐴 ∈ V
spcv.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcev	⊢ (𝜓 → ∃𝑥𝜑)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcev

Step	Hyp	Ref	Expression
1		spcv.1	. 2 ⊢ 𝐴 ∈ V
2		spcv.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	spcegv 3502	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ∃wex 1787   ∈ wcel 2112  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-clel 2809

This theorem is referenced by:  dtruALT  5266  sels  5311  elALT  5312  dtruALT2  5313  nnullss  5331  exss  5332  euotd  5381  opeldm  5761  elrnmpt1  5812  xpnz  6002  ssimaex  6774  fvelrn  6875  dff3  6897  exfo  6902  eufnfv  7023  elunirn  7042  fsnex  7071  f1prex  7072  foeqcnvco  7088  ffoss  7697  op1steq  7783  frxp  7871  suppimacnv  7894  seqomlem2  8165  domtr  8659  en1  8676  en1OLD  8677  enfixsn  8732  php3  8810  1sdom  8857  isinf  8867  ssfiOLD  8873  ac6sfi  8893  hartogslem1  9136  brwdom2  9167  inf0  9214  axinf2  9233  cnfcom3clem  9298  trpredpred  9311  tz9.1c  9324  rankuni  9444  scott0  9467  bnd2  9474  cardprclem  9560  dfac4  9701  dfac5lem5  9706  dfac5  9707  dfac2a  9708  dfac2b  9709  kmlem2  9730  kmlem13  9741  ackbij2  9822  cfsuc  9836  cfflb  9838  cfss  9844  cfsmolem  9849  cfcoflem  9851  fin23lem32  9923  axcc2lem  10015  axcc3  10017  axdc2lem  10027  axdc3lem2  10030  axcclem  10036  brdom3  10107  brdom7disj  10110  brdom6disj  10111  axpowndlem3  10178  canthnumlem  10227  canthp1lem2  10232  inar1  10354  recmulnq  10543  ltexnq  10554  halfnq  10555  ltbtwnnq  10557  1idpr  10608  ltexprlem7  10621  reclem2pr  10627  reclem3pr  10628  sup2  11753  nnunb  12051  uzrdgfni  13496  axdc4uzlem  13521  rtrclreclem3  14588  ntrivcvgmullem  15428  fprodntriv  15467  cnso  15771  vdwapun  16490  vdwlem1  16497  vdwlem12  16508  vdwlem13  16509  isacs2  17110  equivestrcsetc  17613  psgneu  18852  efglem  19060  lmisfree  20758  toprntopon  21776  neitr  22031  cmpsublem  22250  cmpsub  22251  bwth  22261  1stcfb  22296  unisngl  22378  alexsubALTlem3  22900  alexsubALTlem4  22901  vitali  24464  mbfi1fseqlem6  24572  mbfi1flimlem  24574  aannenlem2  25176  istrkg2ld  26505  axlowdim  27006  wlkswwlksf1o  27917  clwlkclwwlkf  28045  padct  30728  cnvoprabOLD  30729  f1ocnt  30797  cycpmconjslem2  31095  locfinreflem  31458  locfinref  31459  prsdm  31532  prsrn  31533  eulerpart  32015  fineqvac  32733  satf0op  33006  prv1n  33060  nosupno  33592  nosupfv  33595  noinfno  33607  noinffv  33610  fnsingle  33907  finminlem  34193  filnetlem3  34255  cnndvlem2  34404  bj-restpw  34947  bj-rest0  34948  exrecfnlem  35236  ctbssinf  35263  poimirlem2  35465  mblfinlem3  35502  mblfinlem4  35503  ismblfin  35504  itg2addnclem  35514  itg2addnc  35517  indexdom  35578  sdclem2  35586  fdc  35589  prtlem16  36569  dihglblem2aN  38993  sn-sup2  40088  eldioph2lem2  40227  dford3lem2  40493  aomclem7  40529  dfac11  40531  rclexi  40840  trclexi  40845  rtrclexi  40846  fnchoice  42186  ssnnf1octb  42347  fzisoeu  42453  stoweidlem28  43187  nnfoctbdjlem  43611  smfpimcclem  43955  funressndmafv2rn  44330  mof0  45781  setc2othin  45953  setrec1lem3  46009  setrec2lem2  46014