Theorem sbequ2 1650

Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sbequ2	|- (x = y -> ([y / x]ph -> ph))

Proof of Theorem sbequ2

Step	Hyp	Ref	Expression
1		df-sb 1649	. 2 |- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
2		simpl 443	. . 3 |- (((x = y -> ph) /\ E.x(x = y /\ ph)) -> (x = y -> ph))
3	2	com12 27	. 2 |- (x = y -> (((x = y -> ph) /\ E.x(x = y /\ ph)) -> ph))
4	1, 3	syl5bi 208	1 |- (x = y -> ([y / x]ph -> ph))

This proof depends on syntax axioms:   -> wi 4   /\ wa 358  E.wex 1541  [wsb 1648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-an 360  df-sb 1649

This theorem is used by:  stdpc7  1917  sbequ12  1919  dfsb2  2055  sbequi  2059  sbn  2062  sbi1  2063  mo  2226  mopick  2266