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

Theorem sb2 1976
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 1728 . 2  |-  ( A. x ( x  =  y  ->  ph )  -> 
( x  =  y  ->  ph ) )
2 equs4 1912 . 2  |-  ( A. x ( x  =  y  ->  ph )  ->  E. x ( x  =  y  /\  ph )
)
3 df-sb 1639 . 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 1530   E.wex 1531   [wsb 1638
This theorem is referenced by:  stdpc4  1977  equsb1  1987  equsb2  1988  sbied  1989  sb6f  1992  hbsb2a  1994  hbsb2e  1995  sb3  2005  sb4b  2007  dfsb2  2008  hbsb2  2010  sbn  2015  sbi1  2016  sb6rf  2044  sbal1  2078  iota4  5253  sbeqal1  27700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639
  Copyright terms: Public domain W3C validator