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

Theorem spcev 3290
 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 3284 . 2 (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
41, 3ax-mp 5 1 (𝜓 → ∃𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480  ∃wex 1701   ∈ wcel 1987  Vcvv 3190 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192 This theorem is referenced by:  dtruALT  4870  elALT  4881  dtruALT2  4882  nnullss  4901  exss  4902  euotd  4945  opeldm  5298  elrnmpt1  5344  xpnz  5522  ssimaex  6230  fvelrn  6318  dff3  6338  exfo  6343  eufnfv  6456  elunirn  6474  fsnex  6503  f1prex  6504  foeqcnvco  6520  snnexOLD  6931  ffoss  7089  op1steq  7170  frxp  7247  suppimacnv  7266  seqomlem2  7506  domtr  7969  ensn1  7980  en1  7983  enfixsn  8029  php3  8106  1sdom  8123  isinf  8133  ssfi  8140  ac6sfi  8164  hartogslem1  8407  brwdom2  8438  inf0  8478  axinf2  8497  cnfcom3clem  8562  tz9.1  8565  tz9.1c  8566  rankuni  8686  scott0  8709  cplem2  8713  bnd2  8716  karden  8718  cardprclem  8765  dfac4  8905  dfac5lem5  8910  dfac5  8911  dfac2a  8912  dfac2  8913  kmlem2  8933  kmlem13  8944  ackbij2  9025  cfsuc  9039  cfflb  9041  cfss  9047  cfsmolem  9052  cfcoflem  9054  fin23lem32  9126  axcc2lem  9218  axcc3  9220  axdc2lem  9230  axdc3lem2  9233  axcclem  9239  brdom3  9310  brdom7disj  9313  brdom6disj  9314  axpowndlem3  9381  canthnumlem  9430  canthp1lem2  9435  inar1  9557  recmulnq  9746  ltexnq  9757  halfnq  9758  ltbtwnnq  9760  1idpr  9811  ltexprlem7  9824  reclem2pr  9830  reclem3pr  9831  sup2  10939  nnunb  11248  uzrdgfni  12713  axdc4uzlem  12738  rtrclreclem3  13750  ntrivcvgmullem  14577  fprodntriv  14616  cnso  14920  vdwapun  15621  vdwlem1  15628  vdwlem12  15639  vdwlem13  15640  isacs2  16254  equivestrcsetc  16732  psgneu  17866  efglem  18069  lmisfree  20121  toprntopon  20669  neitr  20924  cmpsublem  21142  cmpsub  21143  bwth  21153  1stcfb  21188  unisngl  21270  alexsubALTlem3  21793  alexsubALTlem4  21794  vitali  23322  mbfi1fseqlem6  23427  mbfi1flimlem  23429  aannenlem2  24022  istrkg2ld  25293  axlowdim  25775  wlkpwwlkf1ouspgr  26668  wlkisowwlkupgr  26669  padct  29381  cnvoprab  29382  f1ocnt  29442  locfinreflem  29731  locfinref  29732  prsdm  29784  prsrn  29785  eulerpart  30267  bnj150  30707  trpredpred  31482  nosino  31628  nosifv  31629  fnsingle  31721  finminlem  32007  filnetlem3  32070  cnndvlem2  32224  bj-restpw  32735  bj-rest0  32736  poimirlem2  33082  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  itg2addnclem  33132  itg2addnc  33135  indexdom  33200  sdclem2  33209  fdc  33212  prtlem16  33673  dihglblem2aN  36101  eldioph2lem2  36843  dford3lem2  37113  aomclem7  37149  dfac11  37151  relintabex  37407  rclexi  37442  trclexi  37447  rtrclexi  37448  fnchoice  38710  ssnnf1octb  38891  fzisoeu  39013  stoweidlem28  39582  nnfoctbdjlem  40009  smfpimcclem  40350  setrec1lem3  41759  setrec2lem2  41764
 Copyright terms: Public domain W3C validator