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

Theorem sbequ2 1640
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )

Proof of Theorem sbequ2
StepHypRef Expression
1 df-sb 1639 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
2 simpl 443 . . 3  |-  ( ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
)  ->  ( x  =  y  ->  ph )
)
32com12 27 . 2  |-  ( x  =  y  ->  (
( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
)  ->  ph ) )
41, 3syl5bi 208 1  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531   [wsb 1638
This theorem is referenced by:  stdpc7  1870  sbequ12  1872  dfsb2  2008  sbequi  2012  sbn  2015  sbi1  2016  mo  2178  mopick  2218  2pm13.193  28617  2pm13.193VD  28995  sbnNEW7  29537  sbi1NEW7  29538  sbequiNEW7  29553  dfsb2NEW7  29609
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-sb 1639
  Copyright terms: Public domain W3C validator