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

Theorem spcv 3197
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 3191 . 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 1372    = wceq 1374    e. wcel 1762   _Vcvv 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108
This theorem is referenced by:  morex  3280  rext  4688  relop  5144  frxp  6883  pssnn  7728  findcard  7748  fiint  7786  marypha1lem  7882  dfom3  8053  elom3  8054  aceq3lem  8490  dfac3  8491  dfac5lem4  8496  dfac8  8504  dfac9  8505  dfacacn  8510  dfac13  8511  kmlem1  8519  kmlem10  8528  fin23lem34  8715  fin23lem35  8716  zorn2lem7  8871  zornn0g  8874  axgroth6  9195  nnunb  10780  symggen  16284  gsumval3OLD  16692  gsumval3lem2  16694  gsumzaddlem  16718  gsumzaddlemOLD  16720  dfac14  19847  i1fd  21816  chlimi  25814  ddemeas  27834  dfpo2  28747  dfon2lem4  28781  dfon2lem5  28782  dfon2lem7  28784  ttac  30571  dfac11  30601  dfac21  30605
  Copyright terms: Public domain W3C validator