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  17590  equivestrcsetc  18089  psgneu  19412  efglem  19622  lmisfree  21727  toprntopon  22788  neitr  23043  cmpsublem  23262  cmpsub  23263  bwth  23273  1stcfb  23308  unisngl  23390  alexsubALTlem3  23912  alexsubALTlem4  23913  vitali  25490  mbfi1fseqlem6  25597  mbfi1flimlem  25599  aannenlem2  26213  nosupno  27591  nosupfv  27594  noinfno  27606  noinffv  27609  noseqrdgfn  28176  istrkg2ld  28363  axlowdim  28864  wlkswwlksf1o  29782  clwlkclwwlkf  29910  padct  32616  f1ocnt  32698  cycpmconjslem2  33085  locfinreflem  33803  locfinref  33804  prsdm  33877  prsrn  33878  eulerpart  34346  fineqvac  35060  satf0op  35337  prv1n  35391  fnsingle  35880  finminlem  36279  filnetlem3  36341  cnndvlem2  36499  bj-restpw  37053  bj-rest0  37054  exrecfnlem  37340  ctbssinf  37367  poimirlem2  37589  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  itg2addnclem  37638  itg2addnc  37641  indexdom  37701  sdclem2  37709  fdc  37712  prtlem16  38835  dihglblem2aN  41260  sn-sup2  42452  eldioph2lem2  42722  dford3lem2  42989  aomclem7  43022  dfac11  43024  rclexi  43577  trclexi  43582  rtrclexi  43583  permaxinf2lem  44975  permac8prim  44977  fnchoice  44996  ssnnf1octb  45161  fzisoeu  45271  stoweidlem28  45999  nnfoctbdjlem  46426  smfpimcclem  46778  funressndmafv2rn  47197  mof0  48799  nelsubc3lem  49032  initc  49053  setc2othin  49428  cnelsubclem  49565  setrec1lem3  49651  setrec2lem2  49656