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

Theorem spv 2003
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 198 . 2  |-  ( x  =  y  ->  ( ph  ->  ps ) )
32spimv 1995 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1540
This theorem is referenced by:  chvarv  2018  ax10-16  2195  ru  3066  nalset  4232  tfisi  4731  isowe2  5934  findcard2  7188  marypha1lem  7276  setind  7509  karden  7655  kmlem4  7869  axgroth3  8543  ramcl  13173  alexsubALTlem3  17845  i1fd  19140  dfpo2  24670  dfon2lem6  24702  trer  25551
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545
  Copyright terms: Public domain W3C validator