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

Theorem spv 1966
Description: Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
spv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spv  |-  ( A. x ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x, y)    ps( y)

Proof of Theorem spv
StepHypRef Expression
1 spv.1 . . 3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
21biimpd 200 . 2  |-  ( x  =  y  ->  ( ph  ->  ps ) )
32spimv 1964 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550
This theorem is referenced by:  chvarvOLD  1971  ax10-16  2269  ru  3162  nalset  4343  tfisi  4841  isowe2  6073  findcard2  7351  marypha1lem  7441  setind  7676  karden  7824  kmlem4  8038  axgroth3  8711  ramcl  13402  alexsubALTlem3  18085  i1fd  19576  dfpo2  25383  dfon2lem6  25420  trer  26333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator