Theorem spcev 3606

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-clel 2816

This theorem is referenced by:  dtruALT  5388  nnullss  5467  exss  5468  euotd  5518  opeldm  5918  elrnmpt1  5971  xpnz  6179  ssimaex  6994  fvelrn  7096  dff3  7120  exfo  7125  eufnfv  7249  elunirn  7271  fsnex  7303  f1prex  7304  foeqcnvco  7320  ffoss  7970  op1steq  8058  frxp  8151  suppimacnv  8199  seqomlem2  8491  domtr  9047  en1  9064  enfixsn  9121  ssfiALT  9214  php3  9249  php3OLD  9261  1sdomOLD  9285  isinf  9296  isinfOLD  9297  ac6sfi  9320  hartogslem1  9582  brwdom2  9613  inf0  9661  axinf2  9680  cnfcom3clem  9745  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  tz9.1c  9770  rankuni  9903  scott0  9926  bnd2  9933  cardprclem  10019  dfac4  10162  dfac5lem5  10167  dfac5  10169  dfac2a  10170  dfac2b  10171  kmlem2  10192  kmlem13  10203  ackbij2  10282  cfsuc  10297  cfflb  10299  cfss  10305  cfsmolem  10310  cfcoflem  10312  fin23lem32  10384  axcc2lem  10476  axcc3  10478  axdc2lem  10488  axdc3lem2  10491  axcclem  10497  brdom3  10568  brdom7disj  10571  brdom6disj  10572  axpowndlem3  10639  canthnumlem  10688  canthp1lem2  10693  inar1  10815  recmulnq  11004  ltexnq  11015  halfnq  11016  ltbtwnnq  11018  1idpr  11069  ltexprlem7  11082  reclem2pr  11088  reclem3pr  11089  sup2  12224  nnunb  12522  uzrdgfni  13999  axdc4uzlem  14024  rtrclreclem3  15099  ntrivcvgmullem  15937  fprodntriv  15978  cnso  16283  vdwapun  17012  vdwlem1  17019  vdwlem12  17030  vdwlem13  17031  isacs2  17696  equivestrcsetc  18197  psgneu  19524  efglem  19734  lmisfree  21862  toprntopon  22931  neitr  23188  cmpsublem  23407  cmpsub  23408  bwth  23418  1stcfb  23453  unisngl  23535  alexsubALTlem3  24057  alexsubALTlem4  24058  vitali  25648  mbfi1fseqlem6  25755  mbfi1flimlem  25757  aannenlem2  26371  nosupno  27748  nosupfv  27751  noinfno  27763  noinffv  27766  noseqrdgfn  28312  istrkg2ld  28468  axlowdim  28976  wlkswwlksf1o  29899  clwlkclwwlkf  30027  padct  32731  f1ocnt  32804  cycpmconjslem2  33175  locfinreflem  33839  locfinref  33840  prsdm  33913  prsrn  33914  eulerpart  34384  fineqvac  35111  satf0op  35382  prv1n  35436  fnsingle  35920  finminlem  36319  filnetlem3  36381  cnndvlem2  36539  bj-restpw  37093  bj-rest0  37094  exrecfnlem  37380  ctbssinf  37407  poimirlem2  37629  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnc  37681  indexdom  37741  sdclem2  37749  fdc  37752  prtlem16  38870  dihglblem2aN  41295  sn-sup2  42501  eldioph2lem2  42772  dford3lem2  43039  aomclem7  43072  dfac11  43074  rclexi  43628  trclexi  43633  rtrclexi  43634  fnchoice  45034  ssnnf1octb  45199  fzisoeu  45312  stoweidlem28  46043  nnfoctbdjlem  46470  smfpimcclem  46822  funressndmafv2rn  47235  mof0  48747  setc2othin  49113  setrec1lem3  49208  setrec2lem2  49213