Theorem spcev 3556

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  dtruALT  5324  nnullss  5400  exss  5401  euotd  5451  opeldm  5846  elrnmpt1  5899  xpnz  6106  ssimaex  6907  fvelrn  7009  dff3  7033  exfo  7038  eufnfv  7163  elunirn  7185  fsnex  7217  f1prex  7218  foeqcnvco  7234  ffoss  7878  op1steq  7965  frxp  8056  suppimacnv  8104  seqomlem2  8370  domtr  8929  en1  8946  enfixsn  8999  ssfiALT  9083  php3  9118  isinf  9149  ac6sfi  9168  hartogslem1  9428  brwdom2  9459  inf0  9511  axinf2  9530  cnfcom3clem  9595  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  ttrclselem2  9616  tz9.1c  9620  rankuni  9756  scott0  9779  bnd2  9786  cardprclem  9872  dfac4  10013  dfac5lem5  10018  dfac5  10020  dfac2a  10021  dfac2b  10022  kmlem2  10043  kmlem13  10054  ackbij2  10133  cfsuc  10148  cfflb  10150  cfss  10156  cfsmolem  10161  cfcoflem  10163  fin23lem32  10235  axcc2lem  10327  axcc3  10329  axdc2lem  10339  axdc3lem2  10342  axcclem  10348  brdom3  10419  brdom7disj  10422  brdom6disj  10423  axpowndlem3  10490  canthnumlem  10539  canthp1lem2  10544  inar1  10666  recmulnq  10855  ltexnq  10866  halfnq  10867  ltbtwnnq  10869  1idpr  10920  ltexprlem7  10933  reclem2pr  10939  reclem3pr  10940  sup2  12078  nnunb  12377  uzrdgfni  13865  axdc4uzlem  13890  rtrclreclem3  14967  ntrivcvgmullem  15808  fprodntriv  15849  cnso  16156  vdwapun  16886  vdwlem1  16893  vdwlem12  16904  vdwlem13  16905  isacs2  17559  equivestrcsetc  18058  psgneu  19418  efglem  19628  lmisfree  21779  toprntopon  22840  neitr  23095  cmpsublem  23314  cmpsub  23315  bwth  23325  1stcfb  23360  unisngl  23442  alexsubALTlem3  23964  alexsubALTlem4  23965  vitali  25541  mbfi1fseqlem6  25648  mbfi1flimlem  25650  aannenlem2  26264  nosupno  27642  nosupfv  27645  noinfno  27657  noinffv  27660  noseqrdgfn  28236  istrkg2ld  28438  axlowdim  28939  wlkswwlksf1o  29857  clwlkclwwlkf  29988  padct  32701  f1ocnt  32782  cycpmconjslem2  33124  locfinreflem  33853  locfinref  33854  prsdm  33927  prsrn  33928  eulerpart  34395  fineqvac  35139  satf0op  35421  prv1n  35475  fnsingle  35961  finminlem  36360  filnetlem3  36422  cnndvlem2  36580  bj-restpw  37134  bj-rest0  37135  exrecfnlem  37421  ctbssinf  37448  poimirlem2  37670  mblfinlem3  37707  mblfinlem4  37708  ismblfin  37709  itg2addnclem  37719  itg2addnc  37722  indexdom  37782  sdclem2  37790  fdc  37793  prtlem16  38916  dihglblem2aN  41340  sn-sup2  42532  eldioph2lem2  42802  dford3lem2  43068  aomclem7  43101  dfac11  43103  rclexi  43656  trclexi  43661  rtrclexi  43662  permaxinf2lem  45053  permac8prim  45055  fnchoice  45074  ssnnf1octb  45239  fzisoeu  45349  stoweidlem28  46074  nnfoctbdjlem  46501  smfpimcclem  46853  funressndmafv2rn  47262  mof0  48877  nelsubc3lem  49110  initc  49131  setc2othin  49506  cnelsubclem  49643  setrec1lem3  49729  setrec2lem2  49734