Theorem sb2 859

Description: One direction of a simplified definition of substitution.

Assertion

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

Proof of Theorem sb2

Step	Hyp	Ref	Expression
1		ax-4 673	. . 3 ⊢ (∀x(x = y → φ) → (x = y → φ))
2		eqs4 831	. . 3 ⊢ (∀x(x = y → φ) → ∃x(x = y ∧ φ))
3	1, 2	jca 236	. 2 ⊢ (∀x(x = y → φ) → ((x = y → φ) ∧ ∃x(x = y ∧ φ)))
4		df-sb 853	. 2 ⊢ ([y / x]φ ↔ ((x = y → φ) ∧ ∃x(x = y ∧ φ)))
5	3, 4	sylibr 175	1 ⊢ (∀x(x = y → φ) → [y / x]φ)

Syntax hints:   → wi 2   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797  [wsb 852

This theorem is referenced by:  sb3 860  sb4b 862  stdpc4 869  sb6x 871  sb6y 872  hbsb2 873  sbn2 881  sbi1 884  sbt 899  sbeq1 900  sbeq2 901  sbied 903  hbsb4 905  sb5f1 917  sbal1 996

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org