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 ⊢ (𝜓 → ∃𝑥𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-clel 2836

This theorem is used by:  dtruALT  5350  nnullss  5430  exss  5431  euotd  5486  opeldm  5889  elrnmpt1  5942  xpnz  6150  ssimaex  6968  fvelrn  7074  dff3  7098  exfo  7103  eufnfv  7233  elunirn  7253  fsnex  7289  f1prex  7290  foeqcnvco  7306  ffoss  7956  op1steq  8043  frxp  8136  suppimacnv  8184  seqomlem2  8454  domtr  9027  en1  9044  enfixsn  9098  ssfiALT  9182  php3  9217  isinf  9249  ac6sfi  9268  hartogslem1  9529  brwdom2  9560  inf0  9615  axinf2  9634  cnfcom3clem  9699  ssttrcl  9709  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  tz9.1c  9724  rankuni  9872  scott0b  9930  scott0OLD  9931  bnd2  9949  setrec1lem3  9962  setrec2lem2  9969  cardprclem  10053  dfac4  10194  dfac5lem5  10199  dfac5  10200  dfac2a  10201  dfac2b  10202  kmlem2  10223  kmlem13  10234  ackbij2  10313  cfsuc  10328  cfflb  10330  cfss  10336  cfsmolem  10341  cfcoflem  10343  fin23lem32  10415  axcc2lem  10507  axcc3  10509  axdc2lem  10519  axdc3lem2  10522  axcclem  10528  brdom3  10600  brdom7disj  10603  brdom6disj  10604  axpowndlem3  10677  canthnumlem  10726  canthp1lem2  10731  inar1  10853  recmulnq  11042  ltexnq  11053  halfnq  11054  ltbtwnnq  11056  1idpr  11107  ltexprlem7  11120  reclem2pr  11126  reclem3pr  11127  sup2  12266  nnunb  12595  uzrdgfni  14094  axdc4uzlem  14119  rtrclreclem3  15206  ntrivcvgmullem  16063  fprodntriv  16102  cnso  16408  vdwapun  17145  vdwlem1  17152  vdwlem12  17163  vdwlem13  17164  isacs2  17820  equivestrcsetc  18319  psgneu  19713  efglem  19923  lmisfree  22141  toprntopon  23236  neitr  23491  cmpsublem  23710  cmpsub  23711  bwth  23721  1stcfb  23756  unisngl  23839  alexsubALTlem3  24361  alexsubALTlem4  24362  vitali  25927  mbfi1fseqlem6  26034  mbfi1flimlem  26036  aannenlem2  26649  nosupno  28053  nosupfv  28056  noinfno  28068  noinffv  28071  noseqrdgfn  28685  istrkg2ld  28915  axlowdim  29532  wlkswwlksf1o  30461  clwlkclwwlkf  30592  padct  33303  f1ocnt  33385  cycpmconjslem2  33709  locfinreflem  34465  locfinref  34466  prsdm  34539  prsrn  34540  eulerpart  35007  fineqvac  35767  satf0op  36121  prv1n  36175  fnsingle  36661  finminlem  37086  filnetlem3  37148  dfttc4lem1  37296  regsfromregtco  37306  cnndvlem2  37384  bj-restpw  37993  bj-rest0  37994  exrecfnlem  38282  ctbssinf  38309  poimirlem2  38520  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  itg2addnclem  38569  itg2addnc  38572  indexdom  38648  sdclem2  38656  fdc  38659  prtlem16  39906  dihglblem2aN  42330  sn-sup2  43535  eldioph2lem2  43751  dford3lem2  44013  aomclem7  44046  dfac11  44048  rclexi  44600  trclexi  44605  rtrclexi  44606  permaxinf2lem  45980  permac8prim  45982  fnchoice  46015  ssnnf1octb  46178  fzisoeu  46285  stoweidlem28  47007  nnfoctbdjlem  47434  smfpimcclem  47786  funressndmafv2rn  48262  mof0  49917  nelsubc3lem  50147  initc  50168  setc2othin  50543  cnelsubclem  50680