Theorem sb2 1767

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 1510	. 2 |- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
2		equs4 1725	. 2 |- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
3		df-sb 1763	. 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 1492   [wsb 1762

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-i9 1530  ax-ial 1534

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

This theorem is referenced by:  stdpc4  1775  equsb1  1785  equsb2  1786  sbiedh  1787  sb6f  1803  hbsb2a  1806  hbsb2e  1807  sbcof2  1810  sb3  1831  sb4b  1834  sb4bor  1835  hbsb2  1836  nfsb2or  1837  sb6rf  1853  sbi1v  1891  sbalyz  1999  iota4  5197