Theorem spcev 3569

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

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

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 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  dtruALT  5338  nnullss  5417  exss  5418  euotd  5468  opeldm  5861  elrnmpt1  5913  xpnz  6120  ssimaex  6928  fvelrn  7030  dff3  7054  exfo  7059  eufnfv  7185  elunirn  7207  fsnex  7240  f1prex  7241  foeqcnvco  7257  ffoss  7904  op1steq  7991  frxp  8082  suppimacnv  8130  seqomlem2  8396  domtr  8955  en1  8972  enfixsn  9027  ssfiALT  9115  php3  9150  1sdomOLD  9172  isinf  9183  isinfOLD  9184  ac6sfi  9207  hartogslem1  9471  brwdom2  9502  inf0  9550  axinf2  9569  cnfcom3clem  9634  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  tz9.1c  9659  rankuni  9792  scott0  9815  bnd2  9822  cardprclem  9908  dfac4  10051  dfac5lem5  10056  dfac5  10058  dfac2a  10059  dfac2b  10060  kmlem2  10081  kmlem13  10092  ackbij2  10171  cfsuc  10186  cfflb  10188  cfss  10194  cfsmolem  10199  cfcoflem  10201  fin23lem32  10273  axcc2lem  10365  axcc3  10367  axdc2lem  10377  axdc3lem2  10380  axcclem  10386  brdom3  10457  brdom7disj  10460  brdom6disj  10461  axpowndlem3  10528  canthnumlem  10577  canthp1lem2  10582  inar1  10704  recmulnq  10893  ltexnq  10904  halfnq  10905  ltbtwnnq  10907  1idpr  10958  ltexprlem7  10971  reclem2pr  10977  reclem3pr  10978  sup2  12115  nnunb  12414  uzrdgfni  13899  axdc4uzlem  13924  rtrclreclem3  15002  ntrivcvgmullem  15843  fprodntriv  15884  cnso  16191  vdwapun  16921  vdwlem1  16928  vdwlem12  16939  vdwlem13  16940  isacs2  17594  equivestrcsetc  18093  psgneu  19420  efglem  19630  lmisfree  21784  toprntopon  22845  neitr  23100  cmpsublem  23319  cmpsub  23320  bwth  23330  1stcfb  23365  unisngl  23447  alexsubALTlem3  23969  alexsubALTlem4  23970  vitali  25547  mbfi1fseqlem6  25654  mbfi1flimlem  25656  aannenlem2  26270  nosupno  27648  nosupfv  27651  noinfno  27663  noinffv  27666  noseqrdgfn  28240  istrkg2ld  28440  axlowdim  28941  wlkswwlksf1o  29859  clwlkclwwlkf  29987  padct  32693  f1ocnt  32775  cycpmconjslem2  33127  locfinreflem  33823  locfinref  33824  prsdm  33897  prsrn  33898  eulerpart  34366  fineqvac  35080  satf0op  35357  prv1n  35411  fnsingle  35900  finminlem  36299  filnetlem3  36361  cnndvlem2  36519  bj-restpw  37073  bj-rest0  37074  exrecfnlem  37360  ctbssinf  37387  poimirlem2  37609  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  itg2addnclem  37658  itg2addnc  37661  indexdom  37721  sdclem2  37729  fdc  37732  prtlem16  38855  dihglblem2aN  41280  sn-sup2  42472  eldioph2lem2  42742  dford3lem2  43009  aomclem7  43042  dfac11  43044  rclexi  43597  trclexi  43602  rtrclexi  43603  permaxinf2lem  44995  permac8prim  44997  fnchoice  45016  ssnnf1octb  45181  fzisoeu  45291  stoweidlem28  46019  nnfoctbdjlem  46446  smfpimcclem  46798  funressndmafv2rn  47217  mof0  48819  nelsubc3lem  49052  initc  49073  setc2othin  49448  cnelsubclem  49585  setrec1lem3  49671  setrec2lem2  49676