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

Theorem sb1 1662
Description: One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sb1  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph ) )

Proof of Theorem sb1
StepHypRef Expression
1 df-sb 1659 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
21simprbi 451 1  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1550   [wsb 1658
This theorem is referenced by:  spsbe  1663  sb4a  1948  sb4e  1949  sb4  2089  sbftOLD  2104  sbnOLD  2118  sbie  2122  sbiedOLD  2124  sb5rf  2165  sbiedNEW7  29477  sb4NEW7  29489  sbftNEW7  29493  sbnNEW7  29499  sb5rfNEW7  29528
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 1659
  Copyright terms: Public domain W3C validator