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

Theorem sbequ1 1871
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 544 . . 3  |-  ( ( x  =  y  /\  ph )  ->  ( x  =  y  ->  ph )
)
2 19.8a 1730 . . 3  |-  ( ( x  =  y  /\  ph )  ->  E. x
( x  =  y  /\  ph ) )
3 df-sb 1639 . . 3  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
41, 2, 3sylanbrc 645 . 2  |-  ( ( x  =  y  /\  ph )  ->  [ y  /  x ] ph )
54ex 423 1  |-  ( x  =  y  ->  ( ph  ->  [ y  /  x ] ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531   [wsb 1638
This theorem is referenced by:  sbequ12  1872  dfsb2  2008  sbequi  2012  sbn  2015  sbi1  2016  sb6rf  2044  mo  2178  sb5ALT  28587  2pm13.193  28617  2pm13.193VD  28995  sb5ALTVD  29005  sbnNEW7  29537  sbi1NEW7  29538  sbequiNEW7  29553  sb6rfNEW7  29564  dfsb2NEW7  29609
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639
  Copyright terms: Public domain W3C validator