Theorem spcev 3619

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-clel 2819

This theorem is referenced by:  dtruALT  5406  nnullss  5482  exss  5483  euotd  5532  opeldm  5932  elrnmpt1  5983  xpnz  6190  ssimaex  7007  fvelrn  7110  dff3  7134  exfo  7139  eufnfv  7266  elunirn  7288  fsnex  7319  f1prex  7320  foeqcnvco  7336  ffoss  7986  op1steq  8074  frxp  8167  suppimacnv  8215  seqomlem2  8507  domtr  9067  en1  9086  en1OLD  9087  enfixsn  9147  ssfiALT  9241  php3  9275  php3OLD  9287  1sdomOLD  9312  isinf  9323  isinfOLD  9324  ac6sfi  9348  hartogslem1  9611  brwdom2  9642  inf0  9690  axinf2  9709  cnfcom3clem  9774  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  tz9.1c  9799  rankuni  9932  scott0  9955  bnd2  9962  cardprclem  10048  dfac4  10191  dfac5lem5  10196  dfac5  10198  dfac2a  10199  dfac2b  10200  kmlem2  10221  kmlem13  10232  ackbij2  10311  cfsuc  10326  cfflb  10328  cfss  10334  cfsmolem  10339  cfcoflem  10341  fin23lem32  10413  axcc2lem  10505  axcc3  10507  axdc2lem  10517  axdc3lem2  10520  axcclem  10526  brdom3  10597  brdom7disj  10600  brdom6disj  10601  axpowndlem3  10668  canthnumlem  10717  canthp1lem2  10722  inar1  10844  recmulnq  11033  ltexnq  11044  halfnq  11045  ltbtwnnq  11047  1idpr  11098  ltexprlem7  11111  reclem2pr  11117  reclem3pr  11118  sup2  12251  nnunb  12549  uzrdgfni  14009  axdc4uzlem  14034  rtrclreclem3  15109  ntrivcvgmullem  15949  fprodntriv  15990  cnso  16295  vdwapun  17021  vdwlem1  17028  vdwlem12  17039  vdwlem13  17040  isacs2  17711  equivestrcsetc  18221  psgneu  19548  efglem  19758  lmisfree  21885  toprntopon  22952  neitr  23209  cmpsublem  23428  cmpsub  23429  bwth  23439  1stcfb  23474  unisngl  23556  alexsubALTlem3  24078  alexsubALTlem4  24079  vitali  25667  mbfi1fseqlem6  25775  mbfi1flimlem  25777  aannenlem2  26389  nosupno  27766  nosupfv  27769  noinfno  27781  noinffv  27784  noseqrdgfn  28330  istrkg2ld  28486  axlowdim  28994  wlkswwlksf1o  29912  clwlkclwwlkf  30040  padct  32733  cnvoprabOLD  32734  f1ocnt  32807  cycpmconjslem2  33148  locfinreflem  33786  locfinref  33787  prsdm  33860  prsrn  33861  eulerpart  34347  fineqvac  35073  satf0op  35345  prv1n  35399  fnsingle  35883  finminlem  36284  filnetlem3  36346  cnndvlem2  36504  bj-restpw  37058  bj-rest0  37059  exrecfnlem  37345  ctbssinf  37372  poimirlem2  37582  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnc  37634  indexdom  37694  sdclem2  37702  fdc  37705  prtlem16  38825  dihglblem2aN  41250  sn-sup2  42447  eldioph2lem2  42717  dford3lem2  42984  aomclem7  43017  dfac11  43019  rclexi  43577  trclexi  43582  rtrclexi  43583  fnchoice  44929  ssnnf1octb  45101  fzisoeu  45215  stoweidlem28  45949  nnfoctbdjlem  46376  smfpimcclem  46728  funressndmafv2rn  47138  mof0  48551  setc2othin  48723  setrec1lem3  48781  setrec2lem2  48786