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

Theorem spcev 3201
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
spcv.2
Assertion
Ref Expression
spcev
Distinct variable groups:   ,   ,

Proof of Theorem spcev
StepHypRef Expression
1 spcv.1 . 2
2 spcv.2 . . 3
32spcegv 3195 . 2
41, 3ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109
This theorem is referenced by:  dtruALT  4684  elALT  4695  dtruALT2  4696  nnullss  4714  exss  4715  euotd  4753  opeldm  5211  elrnmpt1  5256  xpnz  5431  ssimaex  5938  fvelrn  6024  dff3  6044  exfo  6049  eufnfv  6146  elunirn  6163  foeqcnvco  6203  snnex  6606  ffoss  6761  op1steq  6842  frxp  6910  suppimacnv  6929  seqomlem2  7135  domtr  7588  ensn1  7599  en1  7602  enfixsn  7646  php3  7723  1sdom  7742  isinf  7753  ssfi  7760  ac6sfi  7784  hartogslem1  7988  brwdom2  8020  inf0  8059  axinf2  8078  cnfcom3clem  8170  cnfcom3clemOLD  8178  tz9.1  8181  tz9.1c  8182  rankuni  8302  scott0  8325  cplem2  8329  bnd2  8332  karden  8334  cardprclem  8381  dfac4  8524  dfac5lem5  8529  dfac5  8530  dfac2a  8531  dfac2  8532  kmlem2  8552  kmlem13  8563  ackbij2  8644  cfsuc  8658  cfflb  8660  cfss  8666  cfsmolem  8671  cfcoflem  8673  fin23lem32  8745  axcc2lem  8837  axcc3  8839  axdc2lem  8849  axdc3lem2  8852  axcclem  8858  brdom3  8927  brdom7disj  8930  brdom6disj  8931  axpowndlem3  8996  axpowndlem3OLD  8997  canthnumlem  9047  canthp1lem2  9052  inar1  9174  recmulnq  9363  ltexnq  9374  halfnq  9375  ltbtwnnq  9377  1idpr  9428  ltexprlem7  9441  reclem2pr  9447  reclem3pr  9448  sup2  10524  nnunb  10816  uzrdgfni  12069  axdc4uzlem  12092  ntrivcvgmullem  13710  fprodntriv  13749  cnso  13980  vdwapun  14492  vdwlem1  14499  vdwlem12  14510  vdwlem13  14511  isacs2  15050  psgneu  16531  efglem  16734  lmisfree  18877  neitr  19681  cmpsublem  19899  cmpsub  19900  bwth  19910  1stcfb  19946  unisngl  20028  alexsubALTlem3  20549  alexsubALTlem4  20550  vitali  22022  mbfi1fseqlem6  22127  mbfi1flimlem  22129  aannenlem2  22725  istrkg2ld  23858  axlowdim  24264  cnvoprab  27546  locfinreflem  27843  locfinref  27844  prsdm  27896  prsrn  27897  eulerpart  28321  rtrclreclem.trans  29069  trpredpred  29311  fnsingle  29569  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  itg2addnc  30069  finminlem  30136  filnetlem3  30198  indexdom  30225  sdclem2  30235  fdc  30238  prtlem16  30610  eldioph2lem2  30694  dford3lem2  30969  aomclem7  31006  dfac11  31008  fnchoice  31404  fzisoeu  31500  stoweidlem28  31810  equivestrcsetc  32658  bnj150  33934  dihglblem2aN  37020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111
  Copyright terms: Public domain W3C validator