Theorem spcev 3561

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

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

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  5327  nnullss  5405  exss  5406  euotd  5456  opeldm  5850  elrnmpt1  5902  xpnz  6108  ssimaex  6908  fvelrn  7010  dff3  7034  exfo  7039  eufnfv  7165  elunirn  7187  fsnex  7220  f1prex  7221  foeqcnvco  7237  ffoss  7881  op1steq  7968  frxp  8059  suppimacnv  8107  seqomlem2  8373  domtr  8932  en1  8949  enfixsn  9003  ssfiALT  9088  php3  9123  isinf  9154  ac6sfi  9173  hartogslem1  9434  brwdom2  9465  inf0  9517  axinf2  9536  cnfcom3clem  9601  ssttrcl  9611  ttrcltr  9612  ttrclss  9616  ttrclselem2  9622  tz9.1c  9626  rankuni  9759  scott0  9782  bnd2  9789  cardprclem  9875  dfac4  10016  dfac5lem5  10021  dfac5  10023  dfac2a  10024  dfac2b  10025  kmlem2  10046  kmlem13  10057  ackbij2  10136  cfsuc  10151  cfflb  10153  cfss  10159  cfsmolem  10164  cfcoflem  10166  fin23lem32  10238  axcc2lem  10330  axcc3  10332  axdc2lem  10342  axdc3lem2  10345  axcclem  10351  brdom3  10422  brdom7disj  10425  brdom6disj  10426  axpowndlem3  10493  canthnumlem  10542  canthp1lem2  10547  inar1  10669  recmulnq  10858  ltexnq  10869  halfnq  10870  ltbtwnnq  10872  1idpr  10923  ltexprlem7  10936  reclem2pr  10942  reclem3pr  10943  sup2  12081  nnunb  12380  uzrdgfni  13865  axdc4uzlem  13890  rtrclreclem3  14967  ntrivcvgmullem  15808  fprodntriv  15849  cnso  16156  vdwapun  16886  vdwlem1  16893  vdwlem12  16904  vdwlem13  16905  isacs2  17559  equivestrcsetc  18058  psgneu  19385  efglem  19595  lmisfree  21749  toprntopon  22810  neitr  23065  cmpsublem  23284  cmpsub  23285  bwth  23295  1stcfb  23330  unisngl  23412  alexsubALTlem3  23934  alexsubALTlem4  23935  vitali  25512  mbfi1fseqlem6  25619  mbfi1flimlem  25621  aannenlem2  26235  nosupno  27613  nosupfv  27616  noinfno  27628  noinffv  27631  noseqrdgfn  28205  istrkg2ld  28405  axlowdim  28906  wlkswwlksf1o  29824  clwlkclwwlkf  29952  padct  32662  f1ocnt  32745  cycpmconjslem2  33097  locfinreflem  33807  locfinref  33808  prsdm  33881  prsrn  33882  eulerpart  34350  fineqvac  35072  satf0op  35350  prv1n  35404  fnsingle  35893  finminlem  36292  filnetlem3  36354  cnndvlem2  36512  bj-restpw  37066  bj-rest0  37067  exrecfnlem  37353  ctbssinf  37380  poimirlem2  37602  mblfinlem3  37639  mblfinlem4  37640  ismblfin  37641  itg2addnclem  37651  itg2addnc  37654  indexdom  37714  sdclem2  37722  fdc  37725  prtlem16  38848  dihglblem2aN  41272  sn-sup2  42464  eldioph2lem2  42734  dford3lem2  43000  aomclem7  43033  dfac11  43035  rclexi  43588  trclexi  43593  rtrclexi  43594  permaxinf2lem  44986  permac8prim  44988  fnchoice  45007  ssnnf1octb  45172  fzisoeu  45282  stoweidlem28  46009  nnfoctbdjlem  46436  smfpimcclem  46788  funressndmafv2rn  47207  mof0  48822  nelsubc3lem  49055  initc  49076  setc2othin  49451  cnelsubclem  49588  setrec1lem3  49674  setrec2lem2  49679