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

Theorem spcv 3200
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 3194 . 2  |-  ( A  e.  _V  ->  ( A. x ph  ->  ps ) )
41, 3ax-mp 5 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1393    = wceq 1395    e. wcel 1819   _Vcvv 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111
This theorem is referenced by:  morex  3283  rext  4704  relop  5163  frxp  6909  pssnn  7757  findcard  7777  fiint  7815  marypha1lem  7911  dfom3  8081  elom3  8082  aceq3lem  8518  dfac3  8519  dfac5lem4  8524  dfac8  8532  dfac9  8533  dfacacn  8538  dfac13  8539  kmlem1  8547  kmlem10  8556  fin23lem34  8743  fin23lem35  8744  zorn2lem7  8899  zornn0g  8902  axgroth6  9223  nnunb  10812  symggen  16622  gsumval3OLD  17035  gsumval3lem2  17037  gsumzaddlem  17061  gsumzaddlemOLD  17063  dfac14  20245  i1fd  22214  chlimi  26279  ddemeas  28381  dfpo2  29402  dfon2lem4  29435  dfon2lem5  29436  dfon2lem7  29438  ttac  31182  dfac11  31212  dfac21  31216
  Copyright terms: Public domain W3C validator