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

Theorem spcv 2887
Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
Hypotheses
Ref Expression
spcv.1  |-  A  e. 
_V
spcv.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spcv  |-  ( A. x ph  ->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem spcv
StepHypRef Expression
1 spcv.1 . 2  |-  A  e. 
_V
2 spcv.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32spcgv 2881 . 2  |-  ( A  e.  _V  ->  ( A. x ph  ->  ps ) )
41, 3ax-mp 8 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    = wceq 1632    e. wcel 1696   _Vcvv 2801
This theorem is referenced by:  morex  2962  rext  4238  relop  4850  frxp  6241  pssnn  7097  findcard  7113  fiint  7149  marypha1lem  7202  dfom3  7364  elom3  7365  aceq3lem  7763  dfac3  7764  dfac5lem4  7769  dfac8  7777  dfac9  7778  dfacacn  7783  dfac13  7784  kmlem1  7792  kmlem10  7801  fin23lem34  7988  fin23lem35  7989  zorn2lem7  8145  zornn0g  8148  axgroth6  8466  nnunb  9977  clatl  14236  gsumval3  15207  gsumzaddlem  15219  dfac14  17328  i1fd  19052  chlimi  21830  dfpo2  24183  dfon2lem4  24213  dfon2lem5  24214  dfon2lem7  24216  ttac  27232  dfac11  27263  dfac21  27267  symggen  27514
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803
  Copyright terms: Public domain W3C validator