Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  spcev Structured version   Visualization version   GIF version

Theorem spcev 3555
 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
StepHypRef Expression
1 spcv.1 . 2 𝐴 ∈ V
2 spcv.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32spcegv 3545 . 2 (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
41, 3ax-mp 5 1 (𝜓 → ∃𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3441 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870 This theorem is referenced by:  dtruALT  5254  sels  5299  elALT  5300  dtruALT2  5301  nnullss  5319  exss  5320  euotd  5368  opeldm  5740  elrnmpt1  5794  xpnz  5983  ssimaex  6723  fvelrn  6821  dff3  6843  exfo  6848  eufnfv  6969  elunirn  6988  fsnex  7017  f1prex  7018  foeqcnvco  7034  ffoss  7629  op1steq  7715  frxp  7803  suppimacnv  7824  seqomlem2  8070  domtr  8545  en1  8559  enfixsn  8609  php3  8687  1sdom  8705  isinf  8715  ssfi  8722  ac6sfi  8746  hartogslem1  8990  brwdom2  9021  inf0  9068  axinf2  9087  cnfcom3clem  9152  tz9.1c  9156  rankuni  9276  scott0  9299  bnd2  9306  cardprclem  9392  dfac4  9533  dfac5lem5  9538  dfac5  9539  dfac2a  9540  dfac2b  9541  kmlem2  9562  kmlem13  9573  ackbij2  9654  cfsuc  9668  cfflb  9670  cfss  9676  cfsmolem  9681  cfcoflem  9683  fin23lem32  9755  axcc2lem  9847  axcc3  9849  axdc2lem  9859  axdc3lem2  9862  axcclem  9868  brdom3  9939  brdom7disj  9942  brdom6disj  9943  axpowndlem3  10010  canthnumlem  10059  canthp1lem2  10064  inar1  10186  recmulnq  10375  ltexnq  10386  halfnq  10387  ltbtwnnq  10389  1idpr  10440  ltexprlem7  10453  reclem2pr  10459  reclem3pr  10460  sup2  11584  nnunb  11881  uzrdgfni  13321  axdc4uzlem  13346  rtrclreclem3  14411  ntrivcvgmullem  15249  fprodntriv  15288  cnso  15592  vdwapun  16300  vdwlem1  16307  vdwlem12  16318  vdwlem13  16319  isacs2  16916  equivestrcsetc  17394  psgneu  18626  efglem  18834  lmisfree  20531  toprntopon  21530  neitr  21785  cmpsublem  22004  cmpsub  22005  bwth  22015  1stcfb  22050  unisngl  22132  alexsubALTlem3  22654  alexsubALTlem4  22655  vitali  24217  mbfi1fseqlem6  24324  mbfi1flimlem  24326  aannenlem2  24925  istrkg2ld  26254  axlowdim  26755  wlkswwlksf1o  27665  clwlkclwwlkf  27793  padct  30481  cnvoprabOLD  30482  f1ocnt  30551  cycpmconjslem2  30847  locfinreflem  31193  locfinref  31194  prsdm  31267  prsrn  31268  eulerpart  31750  satf0op  32734  prv1n  32788  trpredpred  33177  nosupno  33313  nosupfv  33316  fnsingle  33490  finminlem  33776  filnetlem3  33838  cnndvlem2  33987  bj-restpw  34504  bj-rest0  34505  exrecfnlem  34793  ctbssinf  34820  poimirlem2  35056  mblfinlem3  35093  mblfinlem4  35094  ismblfin  35095  itg2addnclem  35105  itg2addnc  35108  indexdom  35169  sdclem2  35177  fdc  35180  prtlem16  36162  dihglblem2aN  38586  sn-sup2  39589  eldioph2lem2  39697  dford3lem2  39963  aomclem7  39999  dfac11  40001  rclexi  40310  trclexi  40315  rtrclexi  40316  fnchoice  41653  ssnnf1octb  41817  fzisoeu  41927  stoweidlem28  42665  nnfoctbdjlem  43089  smfpimcclem  43433  funressndmafv2rn  43774  setrec1lem3  45214  setrec2lem2  45219
 Copyright terms: Public domain W3C validator