Theorem spcev 3560

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-clel 2835

This theorem is used by:  dtruALT  5350  nnullss  5430  exss  5431  euotd  5486  opeldm  5890  elrnmpt1  5943  xpnz  6152  ssimaex  6975  fvelrn  7081  dff3  7105  exfo  7110  eufnfv  7239  elunirn  7259  fsnex  7295  f1prex  7296  foeqcnvco  7312  ffoss  7962  op1steq  8049  frxp  8144  suppimacnv  8198  seqomlem2  8468  domtr  9041  en1  9058  enfixsn  9112  ssfiALT  9196  php3  9231  isinf  9263  ac6sfi  9282  hartogslem1  9543  brwdom2  9574  inf0  9629  axinf2  9648  cnfcom3clem  9713  ssttrcl  9723  ttrcltr  9724  ttrclss  9728  ttrclselem2  9734  tz9.1c  9738  rankuni  9886  scott0b  9944  scott0OLD  9945  bnd2  9963  setrec1lem3  9976  setrec2lem2  9983  cardprclem  10067  dfac4  10208  dfac5lem5  10213  dfac5  10214  dfac2a  10215  dfac2b  10216  kmlem2  10237  kmlem13  10248  ackbij2  10327  cfsuc  10342  cfflb  10344  cfss  10350  cfsmolem  10355  cfcoflem  10357  fin23lem32  10429  axcc2lem  10521  axcc3  10523  axdc2lem  10533  axdc3lem2  10536  axcclem  10542  brdom3  10614  brdom7disj  10617  brdom6disj  10618  axpowndlem3  10691  canthnumlem  10740  canthp1lem2  10745  inar1  10867  recmulnq  11056  ltexnq  11067  halfnq  11068  ltbtwnnq  11070  1idpr  11121  ltexprlem7  11134  reclem2pr  11140  reclem3pr  11141  sup2  12280  nnunb  12609  uzrdgfni  14108  axdc4uzlem  14133  rtrclreclem3  15222  ntrivcvgmullem  16079  fprodntriv  16118  cnso  16424  vdwapun  17161  vdwlem1  17168  vdwlem12  17179  vdwlem13  17180  isacs2  17836  equivestrcsetc  18335  psgneu  19729  efglem  19939  lmisfree  22157  toprntopon  23252  neitr  23507  cmpsublem  23726  cmpsub  23727  bwth  23737  1stcfb  23772  unisngl  23855  alexsubALTlem3  24377  alexsubALTlem4  24378  vitali  25943  mbfi1fseqlem6  26050  mbfi1flimlem  26052  aannenlem2  26665  nosupno  28069  nosupfv  28072  noinfno  28084  noinffv  28087  noseqrdgfn  28701  istrkg2ld  28931  axlowdim  29548  wlkswwlksf1o  30477  clwlkclwwlkf  30608  padct  33361  f1ocnt  33442  cycpmconjslem2  33766  locfinreflem  34522  locfinref  34523  prsdm  34596  prsrn  34597  eulerpart  35064  dfac15  35813  weexenwe  35816  fineqvac  35844  vonf1onprcf1ac  35967  onprcf1acwevdlem1  35968  satf0op  36232  prv1n  36286  fnsingle  36777  finminlem  37202  filnetlem3  37264  dfttc4lem1  37412  regsfromregtco  37422  cnndvlem2  37500  bj-restpw  38121  bj-rest0  38122  exrecfnlem  38411  ctbssinf  38438  poimirlem2  38649  mblfinlem3  38686  mblfinlem4  38687  ismblfin  38688  itg2addnclem  38698  itg2addnc  38701  indexdom  38777  sdclem2  38785  fdc  38788  prtlem16  40035  dihglblem2aN  42459  sn-sup2  43664  eldioph2lem2  43881  dford3lem2  44143  aomclem7  44171  dfac11  44173  rclexi  44724  trclexi  44729  rtrclexi  44730  permaxinf2lem  46110  permac8prim  46112  fnchoice  46154  ssnnf1octb  46317  fzisoeu  46424  stoweidlem28  47146  nnfoctbdjlem  47573  smfpimcclem  47925  funressndmafv2rn  48401  mof0  50057  nelsubc3lem  50292  initc  50314  setc2othin  50709  cnelsubcw  50849