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 ⊢ (𝜓 → ∃𝑥𝜑)

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

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 2115

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

This theorem is referenced by:  dtruALT  5333  nnullss  5410  exss  5411  euotd  5461  opeldm  5856  elrnmpt1  5909  xpnz  6117  ssimaex  6919  fvelrn  7021  dff3  7045  exfo  7050  eufnfv  7175  elunirn  7197  fsnex  7229  f1prex  7230  foeqcnvco  7246  ffoss  7890  op1steq  7977  frxp  8068  suppimacnv  8116  seqomlem2  8382  domtr  8944  en1  8961  enfixsn  9014  ssfiALT  9098  php3  9133  isinf  9165  ac6sfi  9184  hartogslem1  9447  brwdom2  9478  inf0  9530  axinf2  9549  cnfcom3clem  9614  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  tz9.1c  9639  rankuni  9775  scott0  9798  bnd2  9805  cardprclem  9891  dfac4  10032  dfac5lem5  10037  dfac5  10039  dfac2a  10040  dfac2b  10041  kmlem2  10062  kmlem13  10073  ackbij2  10152  cfsuc  10167  cfflb  10169  cfss  10175  cfsmolem  10180  cfcoflem  10182  fin23lem32  10254  axcc2lem  10346  axcc3  10348  axdc2lem  10358  axdc3lem2  10361  axcclem  10367  brdom3  10438  brdom7disj  10441  brdom6disj  10442  axpowndlem3  10510  canthnumlem  10559  canthp1lem2  10564  inar1  10686  recmulnq  10875  ltexnq  10886  halfnq  10887  ltbtwnnq  10889  1idpr  10940  ltexprlem7  10953  reclem2pr  10959  reclem3pr  10960  sup2  12098  nnunb  12397  uzrdgfni  13881  axdc4uzlem  13906  rtrclreclem3  14983  ntrivcvgmullem  15824  fprodntriv  15865  cnso  16172  vdwapun  16902  vdwlem1  16909  vdwlem12  16920  vdwlem13  16921  isacs2  17576  equivestrcsetc  18075  psgneu  19435  efglem  19645  lmisfree  21797  toprntopon  22869  neitr  23124  cmpsublem  23343  cmpsub  23344  bwth  23354  1stcfb  23389  unisngl  23471  alexsubALTlem3  23993  alexsubALTlem4  23994  vitali  25570  mbfi1fseqlem6  25677  mbfi1flimlem  25679  aannenlem2  26293  nosupno  27671  nosupfv  27674  noinfno  27686  noinffv  27689  noseqrdgfn  28302  istrkg2ld  28532  axlowdim  29034  wlkswwlksf1o  29952  clwlkclwwlkf  30083  padct  32797  f1ocnt  32880  cycpmconjslem2  33237  locfinreflem  33997  locfinref  33998  prsdm  34071  prsrn  34072  eulerpart  34539  fineqvac  35272  satf0op  35571  prv1n  35625  fnsingle  36111  finminlem  36512  filnetlem3  36574  regsfromregtr  36668  cnndvlem2  36738  bj-restpw  37297  bj-rest0  37298  exrecfnlem  37584  ctbssinf  37611  poimirlem2  37823  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  itg2addnclem  37872  itg2addnc  37875  indexdom  37935  sdclem2  37943  fdc  37946  prtlem16  39129  dihglblem2aN  41553  sn-sup2  42746  eldioph2lem2  43003  dford3lem2  43269  aomclem7  43302  dfac11  43304  rclexi  43856  trclexi  43861  rtrclexi  43862  permaxinf2lem  45253  permac8prim  45255  fnchoice  45274  ssnnf1octb  45438  fzisoeu  45548  stoweidlem28  46272  nnfoctbdjlem  46699  smfpimcclem  47051  funressndmafv2rn  47469  mof0  49083  nelsubc3lem  49315  initc  49336  setc2othin  49711  cnelsubclem  49848  setrec1lem3  49934  setrec2lem2  49939