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

Theorem sb2 1963
Description: One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sb2  |-  ( A. x ( x  =  y  ->  ph )  ->  [ y  /  x ] ph )

Proof of Theorem sb2
StepHypRef Expression
1 sp 1716 . 2  |-  ( A. x ( x  =  y  ->  ph )  -> 
( x  =  y  ->  ph ) )
2 equs4 1899 . 2  |-  ( A. x ( x  =  y  ->  ph )  ->  E. x ( x  =  y  /\  ph )
)
3 df-sb 1630 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
41, 2, 3sylanbrc 645 1  |-  ( A. x ( x  =  y  ->  ph )  ->  [ y  /  x ] ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527   E.wex 1528   [wsb 1629
This theorem is referenced by:  stdpc4  1964  equsb1  1974  equsb2  1975  sbied  1976  sb6f  1979  hbsb2a  1981  hbsb2e  1982  sb3  1992  sb4b  1994  dfsb2  1995  hbsb2  1997  sbn  2002  sbi1  2003  sb6rf  2031  sbal1  2065  iota4  5237  sbeqal1  27597
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630
  Copyright terms: Public domain W3C validator