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

Theorem sbequ2 1657
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 1656 . . 3  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
21simplbi 447 . 2  |-  ( [ y  /  x ] ph  ->  ( x  =  y  ->  ph ) )
32com12 29 1  |-  ( x  =  y  ->  ( [ y  /  x ] ph  ->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547   [wsb 1655
This theorem is referenced by:  stdpc7  1938  sbequ12  1940  dfsb2  2104  sbequi  2108  sbn  2111  sbi1  2112  mo  2276  mopick  2316  2pm13.193  28350  2pm13.193VD  28724  sbnNEW7  29266  sbi1NEW7  29267  sbequiNEW7  29282  dfsb2NEW7  29339
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 178  df-an 361  df-sb 1656
  Copyright terms: Public domain W3C validator