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

Theorem sbequ1 1943
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 1762 . . 3  |-  ( ( x  =  y  /\  ph )  ->  E. x
( x  =  y  /\  ph ) )
3 df-sb 1659 . . 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 1550   [wsb 1658
This theorem is referenced by:  sbequ12  1944  dfsb2  2115  sbnOLD  2118  sbi1  2119  sbequi  2136  sbequiOLD  2137  sb6rf  2166  mo  2302  sb5ALT  28546  2pm13.193  28576  2pm13.193VD  28952  sb5ALTVD  28962  sbnNEW7  29499  sbi1NEW7  29500  sbequiNEW7  29516  sb6rfNEW7  29529  dfsb2NEW7  29575
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659
  Copyright terms: Public domain W3C validator