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

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

Proof of Theorem sb2
StepHypRef Expression
1 sp 1763 . 2  |-  ( A. x ( x  =  y  ->  ph )  -> 
( x  =  y  ->  ph ) )
2 equs4 1997 . 2  |-  ( A. x ( x  =  y  ->  ph )  ->  E. x ( x  =  y  /\  ph )
)
3 df-sb 1659 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
41, 2, 3sylanbrc 646 1  |-  ( A. x ( x  =  y  ->  ph )  ->  [ y  /  x ] ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549   E.wex 1550   [wsb 1658
This theorem is referenced by:  stdpc4  2087  sb3  2088  sb4b  2090  hbsb2  2091  hbsb2a  2093  hbsb2e  2094  equsb1  2113  equsb2  2114  dfsb2  2115  sbnOLD  2118  sbi1  2119  sbie  2122  sbiedOLD  2124  sb6f  2127  sb6rf  2166  sbal1  2202  iota4  5427  sbeqal1  27512
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  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659
  Copyright terms: Public domain W3C validator