Theorem sbequ2 1650

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

Assertion

Ref	Expression
sbequ2	⊢ (x = y → ([y / x]φ → φ))

Proof of Theorem sbequ2

Step	Hyp	Ref	Expression
1		df-sb 1649	. 2 ⊢ ([y / x]φ ↔ ((x = y → φ) ∧ ∃x(x = y ∧ φ)))
2		simpl 443	. . 3 ⊢ (((x = y → φ) ∧ ∃x(x = y ∧ φ)) → (x = y → φ))
3	2	com12 27	. 2 ⊢ (x = y → (((x = y → φ) ∧ ∃x(x = y ∧ φ)) → φ))
4	1, 3	syl5bi 208	1 ⊢ (x = y → ([y / x]φ → φ))

Syntax hints:   → wi 4   ∧ wa 358  ∃wex 1541  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

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