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

Theorem spcev 3273
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 3267 . 2 (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
41, 3ax-mp 5 1 (𝜓 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  wex 1695  wcel 1977  Vcvv 3173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175
This theorem is referenced by:  dtruALT  4821  elALT  4832  dtruALT2  4833  nnullss  4851  exss  4852  euotd  4891  opeldm  5237  elrnmpt1  5282  xpnz  5458  ssimaex  6158  fvelrn  6245  dff3  6265  exfo  6270  eufnfv  6373  elunirn  6391  fsnex  6416  f1prex  6417  foeqcnvco  6433  snnex  6840  ffoss  6998  op1steq  7079  frxp  7152  suppimacnv  7171  seqomlem2  7411  domtr  7873  ensn1  7884  en1  7887  enfixsn  7932  php3  8009  1sdom  8026  isinf  8036  ssfi  8043  ac6sfi  8067  hartogslem1  8308  brwdom2  8339  inf0  8379  axinf2  8398  cnfcom3clem  8463  tz9.1  8466  tz9.1c  8467  rankuni  8587  scott0  8610  cplem2  8614  bnd2  8617  karden  8619  cardprclem  8666  dfac4  8806  dfac5lem5  8811  dfac5  8812  dfac2a  8813  dfac2  8814  kmlem2  8834  kmlem13  8845  ackbij2  8926  cfsuc  8940  cfflb  8942  cfss  8948  cfsmolem  8953  cfcoflem  8955  fin23lem32  9027  axcc2lem  9119  axcc3  9121  axdc2lem  9131  axdc3lem2  9134  axcclem  9140  brdom3  9209  brdom7disj  9212  brdom6disj  9213  axpowndlem3  9278  canthnumlem  9327  canthp1lem2  9332  inar1  9454  recmulnq  9643  ltexnq  9654  halfnq  9655  ltbtwnnq  9657  1idpr  9708  ltexprlem7  9721  reclem2pr  9727  reclem3pr  9728  sup2  10831  nnunb  11138  uzrdgfni  12577  axdc4uzlem  12602  rtrclreclem3  13597  ntrivcvgmullem  14421  fprodntriv  14460  cnso  14764  vdwapun  15465  vdwlem1  15472  vdwlem12  15483  vdwlem13  15484  isacs2  16086  equivestrcsetc  16564  psgneu  17698  efglem  17901  lmisfree  19948  neitr  20742  cmpsublem  20960  cmpsub  20961  bwth  20971  1stcfb  21006  unisngl  21088  alexsubALTlem3  21611  alexsubALTlem4  21612  vitali  23133  mbfi1fseqlem6  23238  mbfi1flimlem  23240  aannenlem2  23833  istrkg2ld  25104  axlowdim  25587  padct  28679  cnvoprab  28680  f1ocnt  28740  locfinreflem  29029  locfinref  29030  prsdm  29082  prsrn  29083  eulerpart  29565  bnj150  29994  trpredpred  30766  fnsingle  30990  finminlem  31276  filnetlem3  31339  cnndvlem2  31493  bj-restpw  32020  bj-rest0  32021  bj-toprntopon  32038  poimirlem2  32375  mblfinlem3  32412  mblfinlem4  32413  ismblfin  32414  itg2addnclem  32425  itg2addnc  32428  indexdom  32493  sdclem2  32502  fdc  32505  prtlem16  32966  dihglblem2aN  35394  eldioph2lem2  36136  dford3lem2  36406  aomclem7  36442  dfac11  36444  relintabex  36700  rclexi  36735  trclexi  36740  rtrclexi  36741  fnchoice  38005  ssnnf1octb  38171  fzisoeu  38249  stoweidlem28  38715  nnfoctbdjlem  39142  1wlkpwwlkf1ouspgr  41068  1wlkisowwlkupgr  41069
  Copyright terms: Public domain W3C validator