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

Theorem spcv 3044
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 3038 . 2  |-  ( A  e.  _V  ->  ( A. x ph  ->  ps ) )
41, 3ax-mp 5 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550    = wceq 1653    e. wcel 1726   _Vcvv 2958
This theorem is referenced by:  morex  3120  rext  4415  relop  5026  frxp  6459  pssnn  7330  findcard  7350  fiint  7386  marypha1lem  7441  dfom3  7605  elom3  7606  aceq3lem  8006  dfac3  8007  dfac5lem4  8012  dfac8  8020  dfac9  8021  dfacacn  8026  dfac13  8027  kmlem1  8035  kmlem10  8044  fin23lem34  8231  fin23lem35  8232  zorn2lem7  8387  zornn0g  8390  axgroth6  8708  nnunb  10222  clatl  14548  gsumval3  15519  gsumzaddlem  15531  dfac14  17655  i1fd  19576  chlimi  22742  dfpo2  25383  dfon2lem4  25418  dfon2lem5  25419  dfon2lem7  25421  ttac  27120  dfac11  27150  dfac21  27154  symggen  27401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960
  Copyright terms: Public domain W3C validator