Theorem sb2 1690

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 1440	. 2 |- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
2		equs4 1653	. 2 |- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
3		df-sb 1686	. 2 |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
4	1, 2, 3	sylanbrc 408	1 |- ( A. x ( x = y -> ph ) -> [ y / x ] ph )

Syntax hints:   -> wi 4   /\ wa 102   A.wal 1282   E.wex 1421   [wsb 1685

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-i9 1463  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-sb 1686

This theorem is referenced by:  stdpc4  1698  equsb1  1708  equsb2  1709  sbiedh  1710  sb6f  1724  hbsb2a  1727  hbsb2e  1728  sbcof2  1731  sb3  1752  sb4b  1755  sb4bor  1756  hbsb2  1757  nfsb2or  1758  sb6rf  1774  sbi1v  1812  sbalyz  1916  iota4  4905