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

Theorem spcv 2874
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 2868 . 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 1527    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  morex  2949  rext  4222  relop  4834  frxp  6225  pssnn  7081  findcard  7097  fiint  7133  marypha1lem  7186  dfom3  7348  elom3  7349  aceq3lem  7747  dfac3  7748  dfac5lem4  7753  dfac8  7761  dfac9  7762  dfacacn  7767  dfac13  7768  kmlem1  7776  kmlem10  7785  fin23lem34  7972  fin23lem35  7973  zorn2lem7  8129  zornn0g  8132  axgroth6  8450  nnunb  9961  clatl  14220  gsumval3  15191  gsumzaddlem  15203  dfac14  17312  i1fd  19036  chlimi  21814  dfpo2  24112  dfon2lem4  24142  dfon2lem5  24143  dfon2lem7  24145  ttac  27129  dfac11  27160  dfac21  27164  symggen  27411
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790
  Copyright terms: Public domain W3C validator