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

Theorem spv 2038
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 207 . 2  |-  ( x  =  y  ->  ( ph  ->  ps ) )
32spimv 2036 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-12 1878  ax-13 2026
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638
This theorem is referenced by:  ru  3276  nalset  4531  isowe2  6229  tfisi  6676  findcard2  7794  marypha1lem  7927  setind  8197  karden  8345  kmlem4  8565  axgroth3  9239  ramcl  14756  alexsubALTlem3  20841  i1fd  22380  dfpo2  29968  dfon2lem6  30007  trer  30544  axc11n-16  31961
  Copyright terms: Public domain W3C validator