Theorem spcev 3605

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-clel 2813

This theorem is referenced by:  dtruALT  5393  nnullss  5472  exss  5473  euotd  5522  opeldm  5920  elrnmpt1  5973  xpnz  6180  ssimaex  6993  fvelrn  7095  dff3  7119  exfo  7124  eufnfv  7248  elunirn  7270  fsnex  7302  f1prex  7303  foeqcnvco  7319  ffoss  7968  op1steq  8056  frxp  8149  suppimacnv  8197  seqomlem2  8489  domtr  9045  en1  9062  enfixsn  9119  ssfiALT  9212  php3  9246  php3OLD  9258  1sdomOLD  9282  isinf  9293  isinfOLD  9294  ac6sfi  9317  hartogslem1  9579  brwdom2  9610  inf0  9658  axinf2  9677  cnfcom3clem  9742  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  tz9.1c  9767  rankuni  9900  scott0  9923  bnd2  9930  cardprclem  10016  dfac4  10159  dfac5lem5  10164  dfac5  10166  dfac2a  10167  dfac2b  10168  kmlem2  10189  kmlem13  10200  ackbij2  10279  cfsuc  10294  cfflb  10296  cfss  10302  cfsmolem  10307  cfcoflem  10309  fin23lem32  10381  axcc2lem  10473  axcc3  10475  axdc2lem  10485  axdc3lem2  10488  axcclem  10494  brdom3  10565  brdom7disj  10568  brdom6disj  10569  axpowndlem3  10636  canthnumlem  10685  canthp1lem2  10690  inar1  10812  recmulnq  11001  ltexnq  11012  halfnq  11013  ltbtwnnq  11015  1idpr  11066  ltexprlem7  11079  reclem2pr  11085  reclem3pr  11086  sup2  12221  nnunb  12519  uzrdgfni  13995  axdc4uzlem  14020  rtrclreclem3  15095  ntrivcvgmullem  15933  fprodntriv  15974  cnso  16279  vdwapun  17007  vdwlem1  17014  vdwlem12  17025  vdwlem13  17026  isacs2  17697  equivestrcsetc  18207  psgneu  19538  efglem  19748  lmisfree  21879  toprntopon  22946  neitr  23203  cmpsublem  23422  cmpsub  23423  bwth  23433  1stcfb  23468  unisngl  23550  alexsubALTlem3  24072  alexsubALTlem4  24073  vitali  25661  mbfi1fseqlem6  25769  mbfi1flimlem  25771  aannenlem2  26385  nosupno  27762  nosupfv  27765  noinfno  27777  noinffv  27780  noseqrdgfn  28326  istrkg2ld  28482  axlowdim  28990  wlkswwlksf1o  29908  clwlkclwwlkf  30036  padct  32736  cnvoprabOLD  32737  f1ocnt  32809  cycpmconjslem2  33157  locfinreflem  33800  locfinref  33801  prsdm  33874  prsrn  33875  eulerpart  34363  fineqvac  35089  satf0op  35361  prv1n  35415  fnsingle  35900  finminlem  36300  filnetlem3  36362  cnndvlem2  36520  bj-restpw  37074  bj-rest0  37075  exrecfnlem  37361  ctbssinf  37388  poimirlem2  37608  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem  37657  itg2addnc  37660  indexdom  37720  sdclem2  37728  fdc  37731  prtlem16  38850  dihglblem2aN  41275  sn-sup2  42477  eldioph2lem2  42748  dford3lem2  43015  aomclem7  43048  dfac11  43050  rclexi  43604  trclexi  43609  rtrclexi  43610  fnchoice  44966  ssnnf1octb  45136  fzisoeu  45250  stoweidlem28  45983  nnfoctbdjlem  46410  smfpimcclem  46762  funressndmafv2rn  47172  mof0  48667  setc2othin  48856  setrec1lem3  48919  setrec2lem2  48924