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

Theorem spcv 3052
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 3046 . 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 1360    = wceq 1362    e. wcel 1755   _Vcvv 2962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964
This theorem is referenced by:  morex  3132  rext  4528  relop  4977  frxp  6671  pssnn  7519  findcard  7539  fiint  7576  marypha1lem  7671  dfom3  7841  elom3  7842  aceq3lem  8278  dfac3  8279  dfac5lem4  8284  dfac8  8292  dfac9  8293  dfacacn  8298  dfac13  8299  kmlem1  8307  kmlem10  8316  fin23lem34  8503  fin23lem35  8504  zorn2lem7  8659  zornn0g  8662  axgroth6  8983  nnunb  10563  symggen  15956  gsumval3OLD  16362  gsumval3lem2  16364  gsumzaddlem  16388  gsumzaddlemOLD  16390  dfac14  19033  i1fd  21001  chlimi  24460  ddemeas  26506  dfpo2  27412  dfon2lem4  27446  dfon2lem5  27447  dfon2lem7  27449  ttac  29230  dfac11  29260  dfac21  29264
  Copyright terms: Public domain W3C validator