Theorem spcev 3549

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  dtruALT  5326  nnullss  5410  exss  5411  euotd  5462  opeldm  5857  elrnmpt1  5910  xpnz  6118  ssimaex  6920  fvelrn  7023  dff3  7047  exfo  7052  eufnfv  7178  elunirn  7200  fsnex  7232  f1prex  7233  foeqcnvco  7249  ffoss  7893  op1steq  7980  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  9536  axinf2  9555  cnfcom3clem  9620  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  tz9.1c  9645  rankuni  9781  scott0  9804  bnd2  9811  cardprclem  9897  dfac4  10038  dfac5lem5  10043  dfac5  10045  dfac2a  10046  dfac2b  10047  kmlem2  10068  kmlem13  10079  ackbij2  10158  cfsuc  10173  cfflb  10175  cfss  10181  cfsmolem  10186  cfcoflem  10188  fin23lem32  10260  axcc2lem  10352  axcc3  10354  axdc2lem  10364  axdc3lem2  10367  axcclem  10373  brdom3  10444  brdom7disj  10447  brdom6disj  10448  axpowndlem3  10516  canthnumlem  10565  canthp1lem2  10570  inar1  10692  recmulnq  10881  ltexnq  10892  halfnq  10893  ltbtwnnq  10895  1idpr  10946  ltexprlem7  10959  reclem2pr  10965  reclem3pr  10966  sup2  12106  nnunb  12427  uzrdgfni  13914  axdc4uzlem  13939  rtrclreclem3  15016  ntrivcvgmullem  15860  fprodntriv  15901  cnso  16208  vdwapun  16939  vdwlem1  16946  vdwlem12  16957  vdwlem13  16958  isacs2  17613  equivestrcsetc  18112  psgneu  19475  efglem  19685  lmisfree  21835  toprntopon  22903  neitr  23158  cmpsublem  23377  cmpsub  23378  bwth  23388  1stcfb  23423  unisngl  23505  alexsubALTlem3  24027  alexsubALTlem4  24028  vitali  25593  mbfi1fseqlem6  25700  mbfi1flimlem  25702  aannenlem2  26309  nosupno  27684  nosupfv  27687  noinfno  27699  noinffv  27702  noseqrdgfn  28315  istrkg2ld  28545  axlowdim  29047  wlkswwlksf1o  29965  clwlkclwwlkf  30096  padct  32809  f1ocnt  32891  cycpmconjslem2  33234  locfinreflem  34003  locfinref  34004  prsdm  34077  prsrn  34078  eulerpart  34545  fineqvac  35279  satf0op  35578  prv1n  35632  fnsingle  36118  finminlem  36519  filnetlem3  36581  dfttc4lem1  36729  regsfromregtco  36739  cnndvlem2  36817  bj-restpw  37423  bj-rest0  37424  exrecfnlem  37712  ctbssinf  37739  poimirlem2  37960  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  itg2addnclem  38009  itg2addnc  38012  indexdom  38072  sdclem2  38080  fdc  38083  prtlem16  39332  dihglblem2aN  41756  sn-sup2  42953  eldioph2lem2  43210  dford3lem2  43476  aomclem7  43509  dfac11  43511  rclexi  44063  trclexi  44068  rtrclexi  44069  permaxinf2lem  45460  permac8prim  45462  fnchoice  45481  ssnnf1octb  45645  fzisoeu  45754  stoweidlem28  46477  nnfoctbdjlem  46904  smfpimcclem  47256  funressndmafv2rn  47686  mof0  49328  nelsubc3lem  49560  initc  49581  setc2othin  49956  cnelsubclem  50093  setrec1lem3  50179  setrec2lem2  50184