Theorem sb2 1820

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 1563	. 2 |- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
2		equs4 1777	. 2 |- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
3		df-sb 1816	. 2 |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
4	1, 2, 3	sylanbrc 421	1 |- ( A. x ( x = y -> ph ) -> [ y / x ] ph )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1400   E.wex 1545   [wsb 1815

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-i9 1583  ax-ial 1587

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

This theorem is referenced by:  stdpc4  1828  equsb1  1838  equsb2  1839  sbiedh  1840  sb6f  1856  hbsb2a  1859  hbsb2e  1860  sbcof2  1863  sb3  1884  sb4b  1887  sb4bor  1888  hbsb2  1889  nfsb2or  1890  sb6rf  1906  sbi1v  1946  sbalyz  2059  iota4  5352