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

Theorem spv 1967
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 1965 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1955
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  axc11n-16  2248  ru  3293  nalset  4540  isowe2  6153  tfisi  6582  findcard2  7666  marypha1lem  7797  setind  8068  karden  8216  kmlem4  8436  axgroth3  9112  ramcl  14211  alexsubALTlem3  19756  i1fd  21295  dfpo2  27729  dfon2lem6  27765  trer  28679
  Copyright terms: Public domain W3C validator