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

Theorem spv 1963
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 199 . 2  |-  ( x  =  y  ->  ( ph  ->  ps ) )
32spimv 1961 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546
This theorem is referenced by:  chvarvOLD  2051  ax10-16  2248  ru  3128  nalset  4308  tfisi  4805  isowe2  6037  findcard2  7315  marypha1lem  7404  setind  7637  karden  7783  kmlem4  7997  axgroth3  8670  ramcl  13360  alexsubALTlem3  18041  i1fd  19534  dfpo2  25334  dfon2lem6  25366  trer  26217
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757  ax-12 1946
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator