Theorem spcev 3572

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

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

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  5343  nnullss  5422  exss  5423  euotd  5473  opeldm  5871  elrnmpt1  5924  xpnz  6132  ssimaex  6946  fvelrn  7048  dff3  7072  exfo  7077  eufnfv  7203  elunirn  7225  fsnex  7258  f1prex  7259  foeqcnvco  7275  ffoss  7924  op1steq  8012  frxp  8105  suppimacnv  8153  seqomlem2  8419  domtr  8978  en1  8995  enfixsn  9050  ssfiALT  9138  php3  9173  1sdomOLD  9196  isinf  9207  isinfOLD  9208  ac6sfi  9231  hartogslem1  9495  brwdom2  9526  inf0  9574  axinf2  9593  cnfcom3clem  9658  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  tz9.1c  9683  rankuni  9816  scott0  9839  bnd2  9846  cardprclem  9932  dfac4  10075  dfac5lem5  10080  dfac5  10082  dfac2a  10083  dfac2b  10084  kmlem2  10105  kmlem13  10116  ackbij2  10195  cfsuc  10210  cfflb  10212  cfss  10218  cfsmolem  10223  cfcoflem  10225  fin23lem32  10297  axcc2lem  10389  axcc3  10391  axdc2lem  10401  axdc3lem2  10404  axcclem  10410  brdom3  10481  brdom7disj  10484  brdom6disj  10485  axpowndlem3  10552  canthnumlem  10601  canthp1lem2  10606  inar1  10728  recmulnq  10917  ltexnq  10928  halfnq  10929  ltbtwnnq  10931  1idpr  10982  ltexprlem7  10995  reclem2pr  11001  reclem3pr  11002  sup2  12139  nnunb  12438  uzrdgfni  13923  axdc4uzlem  13948  rtrclreclem3  15026  ntrivcvgmullem  15867  fprodntriv  15908  cnso  16215  vdwapun  16945  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  isacs2  17614  equivestrcsetc  18113  psgneu  19436  efglem  19646  lmisfree  21751  toprntopon  22812  neitr  23067  cmpsublem  23286  cmpsub  23287  bwth  23297  1stcfb  23332  unisngl  23414  alexsubALTlem3  23936  alexsubALTlem4  23937  vitali  25514  mbfi1fseqlem6  25621  mbfi1flimlem  25623  aannenlem2  26237  nosupno  27615  nosupfv  27618  noinfno  27630  noinffv  27633  noseqrdgfn  28200  istrkg2ld  28387  axlowdim  28888  wlkswwlksf1o  29809  clwlkclwwlkf  29937  padct  32643  f1ocnt  32725  cycpmconjslem2  33112  locfinreflem  33830  locfinref  33831  prsdm  33904  prsrn  33905  eulerpart  34373  fineqvac  35087  satf0op  35364  prv1n  35418  fnsingle  35907  finminlem  36306  filnetlem3  36368  cnndvlem2  36526  bj-restpw  37080  bj-rest0  37081  exrecfnlem  37367  ctbssinf  37394  poimirlem2  37616  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem  37665  itg2addnc  37668  indexdom  37728  sdclem2  37736  fdc  37739  prtlem16  38862  dihglblem2aN  41287  sn-sup2  42479  eldioph2lem2  42749  dford3lem2  43016  aomclem7  43049  dfac11  43051  rclexi  43604  trclexi  43609  rtrclexi  43610  permaxinf2lem  45002  permac8prim  45004  fnchoice  45023  ssnnf1octb  45188  fzisoeu  45298  stoweidlem28  46026  nnfoctbdjlem  46453  smfpimcclem  46805  funressndmafv2rn  47224  mof0  48826  nelsubc3lem  49059  initc  49080  setc2othin  49455  cnelsubclem  49592  setrec1lem3  49678  setrec2lem2  49683