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

Theorem spcv 3200
 Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
Hypotheses
Ref Expression
spcv.1
spcv.2
Assertion
Ref Expression
spcv
Distinct variable groups:   ,   ,

Proof of Theorem spcv
StepHypRef Expression
1 spcv.1 . 2
2 spcv.2 . . 3
32spcgv 3194 . 2
41, 3ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818   cvv 3109 This theorem is referenced by:  morex  3283  rext  4700  relop  5158  frxp  6910  pssnn  7758  findcard  7779  fiint  7817  marypha1lem  7913  dfom3  8085  elom3  8086  aceq3lem  8522  dfac3  8523  dfac5lem4  8528  dfac8  8536  dfac9  8537  dfacacn  8542  dfac13  8543  kmlem1  8551  kmlem10  8560  fin23lem34  8747  fin23lem35  8748  zorn2lem7  8903  zornn0g  8906  axgroth6  9227  nnunb  10816  symggen  16495  gsumval3OLD  16908  gsumval3lem2  16910  gsumzaddlem  16934  gsumzaddlemOLD  16936  dfac14  20119  i1fd  22088  chlimi  26152  ddemeas  28208  dfpo2  29184  dfon2lem4  29218  dfon2lem5  29219  dfon2lem7  29221  ttac  30978  dfac11  31008  dfac21  31012 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