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

Theorem sb2 2094
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 1766 . 2  |-  ( A. x ( x  =  y  ->  ph )  -> 
( x  =  y  ->  ph ) )
2 equs4 2001 . 2  |-  ( A. x ( x  =  y  ->  ph )  ->  E. x ( x  =  y  /\  ph )
)
3 df-sb 1661 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
41, 2, 3sylanbrc 647 1  |-  ( A. x ( x  =  y  ->  ph )  ->  [ y  /  x ] ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   A.wal 1550   E.wex 1551   [wsb 1660
This theorem is referenced by:  stdpc4  2095  sb3  2097  sb4b  2099  hbsb2  2100  hbsb2a  2102  hbsb2e  2103  equsb1  2106  equsb2  2107  dfsb2  2113  sb6f  2127  sbnOLD  2136  sbi1  2137  sbie  2155  sbiedOLD  2158  sb6rf  2174  sbal1  2210  iota4  5471  sbeqal1  27686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-11 1764  ax-12 1954
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1661
  Copyright terms: Public domain W3C validator