ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sb2 Unicode version

Theorem sb2 1725
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 ax-4 1472 . 2  |-  ( A. x ( x  =  y  ->  ph )  -> 
( x  =  y  ->  ph ) )
2 equs4 1688 . 2  |-  ( A. x ( x  =  y  ->  ph )  ->  E. x ( x  =  y  /\  ph )
)
3 df-sb 1721 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
41, 2, 3sylanbrc 413 1  |-  ( A. x ( x  =  y  ->  ph )  ->  [ y  /  x ] ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103   A.wal 1314   E.wex 1453   [wsb 1720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-i9 1495  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-sb 1721
This theorem is referenced by:  stdpc4  1733  equsb1  1743  equsb2  1744  sbiedh  1745  sb6f  1759  hbsb2a  1762  hbsb2e  1763  sbcof2  1766  sb3  1787  sb4b  1790  sb4bor  1791  hbsb2  1792  nfsb2or  1793  sb6rf  1809  sbi1v  1847  sbalyz  1952  iota4  5076
  Copyright terms: Public domain W3C validator