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

Theorem sbequ1 1932
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 1754 . . 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  1933  dfsb2  2090  sbequi  2094  sbn  2097  sbi1  2098  sb6rf  2126  mo  2262  sb5ALT  27954  2pm13.193  27984  2pm13.193VD  28358  sb5ALTVD  28368  sbnNEW7  28900  sbi1NEW7  28901  sbequiNEW7  28916  sb6rfNEW7  28927  dfsb2NEW7  28973
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 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656
  Copyright terms: Public domain W3C validator