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

Theorem spcv 3066
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 3060 . 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 1367    = wceq 1369    e. wcel 1756   _Vcvv 2975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977
This theorem is referenced by:  morex  3146  rext  4543  relop  4993  frxp  6685  pssnn  7534  findcard  7554  fiint  7591  marypha1lem  7686  dfom3  7856  elom3  7857  aceq3lem  8293  dfac3  8294  dfac5lem4  8299  dfac8  8307  dfac9  8308  dfacacn  8313  dfac13  8314  kmlem1  8322  kmlem10  8331  fin23lem34  8518  fin23lem35  8519  zorn2lem7  8674  zornn0g  8677  axgroth6  8998  nnunb  10578  symggen  15979  gsumval3OLD  16385  gsumval3lem2  16387  gsumzaddlem  16411  gsumzaddlemOLD  16413  dfac14  19194  i1fd  21162  chlimi  24640  ddemeas  26655  dfpo2  27568  dfon2lem4  27602  dfon2lem5  27603  dfon2lem7  27605  ttac  29388  dfac11  29418  dfac21  29422
  Copyright terms: Public domain W3C validator