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

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

Proof of Theorem sbequ1
StepHypRef Expression
1 pm3.4 545 . . 3  |-  ( ( x  =  y  /\  ph )  ->  ( x  =  y  ->  ph )
)
2 19.8a 1758 . . 3  |-  ( ( x  =  y  /\  ph )  ->  E. x
( x  =  y  /\  ph ) )
3 df-sb 1656 . . 3  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
41, 2, 3sylanbrc 646 . 2  |-  ( ( x  =  y  /\  ph )  ->  [ y  /  x ] ph )
54ex 424 1  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547   [wsb 1655
This theorem is referenced by:  sbequ12  1940  dfsb2  2104  sbequi  2108  sbn  2111  sbi1  2112  sb6rf  2140  mo  2276  sb5ALT  28320  2pm13.193  28350  2pm13.193VD  28724  sb5ALTVD  28734  sbnNEW7  29266  sbi1NEW7  29267  sbequiNEW7  29282  sb6rfNEW7  29293  dfsb2NEW7  29339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656
  Copyright terms: Public domain W3C validator