Theorem sb2 1765

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

Step	Hyp	Ref	Expression
1		ax-4 1508	. 2 |- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
2		equs4 1723	. 2 |- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
3		df-sb 1761	. 2 |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
4	1, 2, 3	sylanbrc 417	1 |- ( A. x ( x = y -> ph ) -> [ y / x ] ph )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1351   E.wex 1490   [wsb 1760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-i9 1528  ax-ial 1532

This theorem depends on definitions:  df-bi 117  df-sb 1761

This theorem is referenced by:  stdpc4  1773  equsb1  1783  equsb2  1784  sbiedh  1785  sb6f  1801  hbsb2a  1804  hbsb2e  1805  sbcof2  1808  sb3  1829  sb4b  1832  sb4bor  1833  hbsb2  1834  nfsb2or  1835  sb6rf  1851  sbi1v  1889  sbalyz  1997  iota4  5188