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

Theorem spcv 2979
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 2973 . 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 177   A.wal 1546    = wceq 1649    e. wcel 1717   _Vcvv 2893
This theorem is referenced by:  morex  3055  rext  4347  relop  4957  frxp  6386  pssnn  7257  findcard  7277  fiint  7313  marypha1lem  7367  dfom3  7529  elom3  7530  aceq3lem  7928  dfac3  7929  dfac5lem4  7934  dfac8  7942  dfac9  7943  dfacacn  7948  dfac13  7949  kmlem1  7957  kmlem10  7966  fin23lem34  8153  fin23lem35  8154  zorn2lem7  8309  zornn0g  8312  axgroth6  8630  nnunb  10143  clatl  14464  gsumval3  15435  gsumzaddlem  15447  dfac14  17565  i1fd  19434  chlimi  22579  dfpo2  25130  dfon2lem4  25160  dfon2lem5  25161  dfon2lem7  25163  ttac  26792  dfac11  26823  dfac21  26827  symggen  27074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-v 2895
  Copyright terms: Public domain W3C validator