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

Theorem sbequ2 1661
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.)
Assertion
Ref Expression
sbequ2  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )

Proof of Theorem sbequ2
StepHypRef Expression
1 df-sb 1660 . . 3  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
21simplbi 448 . 2  |-  ( [ y  /  x ] ph  ->  ( x  =  y  ->  ph ) )
32com12 30 1  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551   [wsb 1659
This theorem is referenced by:  stdpc7  1943  sbequ12  1945  dfsb2  2110  sbequi  2112  sbequiOLD  2116  sbnOLD  2133  sbi1  2134  mo  2305  mopick  2345  2pm13.193  28641  2pm13.193VD  29017  sbnNEW7  29564  sbi1NEW7  29565  sbequiNEW7  29581  dfsb2NEW7  29640
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 179  df-an 362  df-sb 1660
  Copyright terms: Public domain W3C validator