Theorem spcev 3565

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560  ∃wex 1799   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-clel 2837

This theorem is referenced by:  dtruALT  5345  nnullss  5429  exss  5430  euotd  5482  opeldm  5883  elrnmpt1  5936  xpnz  6144  ssimaex  6952  fvelrn  7057  dff3  7081  exfo  7086  eufnfv  7213  elunirn  7235  fsnex  7267  f1prex  7268  foeqcnvco  7284  ffoss  7927  op1steq  8014  frxp  8106  suppimacnv  8154  seqomlem2  8422  domtr  8988  en1  9005  enfixsn  9058  ssfiALT  9142  php3  9177  isinf  9209  ac6sfi  9228  hartogslem1  9490  brwdom2  9521  inf0  9576  axinf2  9595  cnfcom3clem  9660  ssttrcl  9670  ttrcltr  9671  ttrclss  9675  ttrclselem2  9681  tz9.1c  9685  rankuni  9821  scott0  9844  bnd2  9851  cardprclem  9937  dfac4  10078  dfac5lem5  10083  dfac5  10085  dfac2a  10086  dfac2b  10087  kmlem2  10108  kmlem13  10119  ackbij2  10198  cfsuc  10214  cfflb  10216  cfss  10222  cfsmolem  10227  cfcoflem  10229  fin23lem32  10301  axcc2lem  10393  axcc3  10395  axdc2lem  10405  axdc3lem2  10408  axcclem  10414  brdom3  10485  brdom7disj  10488  brdom6disj  10489  axpowndlem3  10557  canthnumlem  10606  canthp1lem2  10611  inar1  10733  recmulnq  10922  ltexnq  10933  halfnq  10934  ltbtwnnq  10936  1idpr  10987  ltexprlem7  11000  reclem2pr  11006  reclem3pr  11007  sup2  12148  nnunb  12477  uzrdgfni  13971  axdc4uzlem  13996  rtrclreclem3  15073  ntrivcvgmullem  15931  fprodntriv  15972  cnso  16279  vdwapun  17010  vdwlem1  17017  vdwlem12  17028  vdwlem13  17029  isacs2  17685  equivestrcsetc  18184  psgneu  19546  efglem  19756  lmisfree  21894  toprntopon  22985  neitr  23240  cmpsublem  23459  cmpsub  23460  bwth  23470  1stcfb  23505  unisngl  23587  alexsubALTlem3  24109  alexsubALTlem4  24110  vitali  25675  mbfi1fseqlem6  25782  mbfi1flimlem  25784  aannenlem2  26393  nosupno  27767  nosupfv  27770  noinfno  27782  noinffv  27785  noseqrdgfn  28399  istrkg2ld  28629  axlowdim  29162  wlkswwlksf1o  30079  clwlkclwwlkf  30210  padct  32920  f1ocnt  33002  cycpmconjslem2  33335  locfinreflem  34137  locfinref  34138  prsdm  34211  prsrn  34212  eulerpart  34679  fineqvac  35412  satf0op  35727  prv1n  35781  fnsingle  36267  finminlem  36678  filnetlem3  36740  dfttc4lem1  36888  regsfromregtco  36898  cnndvlem2  36976  bj-restpw  37582  bj-rest0  37583  exrecfnlem  37873  ctbssinf  37900  poimirlem2  38121  mblfinlem3  38158  mblfinlem4  38159  ismblfin  38160  itg2addnclem  38170  itg2addnc  38173  indexdom  38233  sdclem2  38241  fdc  38244  prtlem16  39493  dihglblem2aN  41917  sn-sup2  43113  eldioph2lem2  43342  dford3lem2  43604  aomclem7  43637  dfac11  43639  rclexi  44191  trclexi  44196  rtrclexi  44197  permaxinf2lem  45588  permac8prim  45590  fnchoice  45609  ssnnf1octb  45772  fzisoeu  45879  stoweidlem28  46602  nnfoctbdjlem  47029  smfpimcclem  47381  funressndmafv2rn  47817  mof0  49459  nelsubc3lem  49691  initc  49712  setc2othin  50087  cnelsubclem  50224  setrec1lem3  50310  setrec2lem2  50315