Theorem spcev 3546

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ∃wex 1787   ∈ wcel 2121  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-clel 2816

This theorem is referenced by:  dtruALT  5320  nnullss  5404  exss  5405  euotd  5457  opeldm  5856  elrnmpt1  5909  xpnz  6114  ssimaex  6916  fvelrn  7021  dff3  7045  exfo  7050  eufnfv  7177  elunirn  7199  fsnex  7231  f1prex  7232  foeqcnvco  7248  ffoss  7892  op1steq  7979  frxp  8070  suppimacnv  8118  seqomlem2  8384  domtr  8948  en1  8965  enfixsn  9018  ssfiALT  9102  php3  9137  isinf  9169  ac6sfi  9188  hartogslem1  9451  brwdom2  9482  inf0  9537  axinf2  9556  cnfcom3clem  9621  ssttrcl  9631  ttrcltr  9632  ttrclss  9636  ttrclselem2  9642  tz9.1c  9646  rankuni  9782  scott0  9805  bnd2  9812  cardprclem  9898  dfac4  10039  dfac5lem5  10044  dfac5  10046  dfac2a  10047  dfac2b  10048  kmlem2  10069  kmlem13  10080  ackbij2  10159  cfsuc  10174  cfflb  10176  cfss  10182  cfsmolem  10187  cfcoflem  10189  fin23lem32  10261  axcc2lem  10353  axcc3  10355  axdc2lem  10365  axdc3lem2  10368  axcclem  10374  brdom3  10445  brdom7disj  10448  brdom6disj  10449  axpowndlem3  10517  canthnumlem  10566  canthp1lem2  10571  inar1  10693  recmulnq  10882  ltexnq  10893  halfnq  10894  ltbtwnnq  10896  1idpr  10947  ltexprlem7  10960  reclem2pr  10966  reclem3pr  10967  sup2  12107  nnunb  12428  uzrdgfni  13915  axdc4uzlem  13940  rtrclreclem3  15017  ntrivcvgmullem  15861  fprodntriv  15902  cnso  16209  vdwapun  16940  vdwlem1  16947  vdwlem12  16958  vdwlem13  16959  isacs2  17614  equivestrcsetc  18113  psgneu  19476  efglem  19686  lmisfree  21821  toprntopon  22912  neitr  23167  cmpsublem  23386  cmpsub  23387  bwth  23397  1stcfb  23432  unisngl  23514  alexsubALTlem3  24036  alexsubALTlem4  24037  vitali  25602  mbfi1fseqlem6  25709  mbfi1flimlem  25711  aannenlem2  26317  nosupno  27689  nosupfv  27692  noinfno  27704  noinffv  27707  noseqrdgfn  28320  istrkg2ld  28550  axlowdim  29052  wlkswwlksf1o  29969  clwlkclwwlkf  30100  padct  32814  f1ocnt  32896  cycpmconjslem2  33240  locfinreflem  34036  locfinref  34037  prsdm  34110  prsrn  34111  eulerpart  34578  fineqvac  35312  satf0op  35620  prv1n  35674  fnsingle  36160  finminlem  36561  filnetlem3  36623  dfttc4lem1  36771  regsfromregtco  36781  cnndvlem2  36859  bj-restpw  37465  bj-rest0  37466  exrecfnlem  37756  ctbssinf  37783  poimirlem2  38004  mblfinlem3  38041  mblfinlem4  38042  ismblfin  38043  itg2addnclem  38053  itg2addnc  38056  indexdom  38116  sdclem2  38124  fdc  38127  prtlem16  39376  dihglblem2aN  41800  sn-sup2  42996  eldioph2lem2  43225  dford3lem2  43487  aomclem7  43520  dfac11  43522  rclexi  44074  trclexi  44079  rtrclexi  44080  permaxinf2lem  45471  permac8prim  45473  fnchoice  45492  ssnnf1octb  45655  fzisoeu  45762  stoweidlem28  46485  nnfoctbdjlem  46912  smfpimcclem  47264  funressndmafv2rn  47700  mof0  49342  nelsubc3lem  49574  initc  49595  setc2othin  49970  cnelsubclem  50107  setrec1lem3  50193  setrec2lem2  50198