Theorem spcev 3543

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 3534	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∃wex 1785   ∈ wcel 2109  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-clel 2817

This theorem is referenced by:  dtruALT  5314  sels  5359  elALT  5360  dtruALT2  5361  nnullss  5379  exss  5380  euotd  5429  opeldm  5813  elrnmpt1  5864  xpnz  6059  ssimaex  6847  fvelrn  6948  dff3  6970  exfo  6975  eufnfv  7099  elunirn  7118  fsnex  7148  f1prex  7149  foeqcnvco  7165  ffoss  7775  op1steq  7861  frxp  7951  suppimacnv  7974  seqomlem2  8266  domtr  8764  en1  8781  en1OLD  8782  enfixsn  8837  ssfiALT  8922  php3  8959  php3OLD  8972  1sdom  8987  isinf  8997  ac6sfi  9019  hartogslem1  9262  brwdom2  9293  inf0  9340  axinf2  9359  cnfcom3clem  9424  ssttrcl  9434  ttrcltr  9435  ttrclss  9439  ttrclselem2  9445  trpredpred  9458  tz9.1c  9471  rankuni  9605  scott0  9628  bnd2  9635  cardprclem  9721  dfac4  9862  dfac5lem5  9867  dfac5  9868  dfac2a  9869  dfac2b  9870  kmlem2  9891  kmlem13  9902  ackbij2  9983  cfsuc  9997  cfflb  9999  cfss  10005  cfsmolem  10010  cfcoflem  10012  fin23lem32  10084  axcc2lem  10176  axcc3  10178  axdc2lem  10188  axdc3lem2  10191  axcclem  10197  brdom3  10268  brdom7disj  10271  brdom6disj  10272  axpowndlem3  10339  canthnumlem  10388  canthp1lem2  10393  inar1  10515  recmulnq  10704  ltexnq  10715  halfnq  10716  ltbtwnnq  10718  1idpr  10769  ltexprlem7  10782  reclem2pr  10788  reclem3pr  10789  sup2  11914  nnunb  12212  uzrdgfni  13659  axdc4uzlem  13684  rtrclreclem3  14752  ntrivcvgmullem  15594  fprodntriv  15633  cnso  15937  vdwapun  16656  vdwlem1  16663  vdwlem12  16674  vdwlem13  16675  isacs2  17343  equivestrcsetc  17850  psgneu  19095  efglem  19303  lmisfree  21030  toprntopon  22055  neitr  22312  cmpsublem  22531  cmpsub  22532  bwth  22542  1stcfb  22577  unisngl  22659  alexsubALTlem3  23181  alexsubALTlem4  23182  vitali  24758  mbfi1fseqlem6  24866  mbfi1flimlem  24868  aannenlem2  25470  istrkg2ld  26802  axlowdim  27310  wlkswwlksf1o  28223  clwlkclwwlkf  28351  padct  31033  cnvoprabOLD  31034  f1ocnt  31102  cycpmconjslem2  31401  locfinreflem  31769  locfinref  31770  prsdm  31843  prsrn  31844  eulerpart  32328  fineqvac  33045  satf0op  33318  prv1n  33372  nosupno  33885  nosupfv  33888  noinfno  33900  noinffv  33903  fnsingle  34200  finminlem  34486  filnetlem3  34548  cnndvlem2  34697  bj-restpw  35242  bj-rest0  35243  exrecfnlem  35529  ctbssinf  35556  poimirlem2  35758  mblfinlem3  35795  mblfinlem4  35796  ismblfin  35797  itg2addnclem  35807  itg2addnc  35810  indexdom  35871  sdclem2  35879  fdc  35882  prtlem16  36862  dihglblem2aN  39286  sn-sup2  40419  eldioph2lem2  40563  dford3lem2  40829  aomclem7  40865  dfac11  40867  rclexi  41176  trclexi  41181  rtrclexi  41182  fnchoice  42525  ssnnf1octb  42686  fzisoeu  42793  stoweidlem28  43523  nnfoctbdjlem  43947  smfpimcclem  44291  funressndmafv2rn  44666  mof0  46117  setc2othin  46289  setrec1lem3  46347  setrec2lem2  46352