Theorem sb2 2023

Description: One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem sb2

Step	Hyp	Ref	Expression
1		sp 1747	. 2 ⊢ (∀x(x = y → φ) → (x = y → φ))
2		equs4 1959	. 2 ⊢ (∀x(x = y → φ) → ∃x(x = y ∧ φ))
3		df-sb 1649	. 2 ⊢ ([y / x]φ ↔ ((x = y → φ) ∧ ∃x(x = y ∧ φ)))
4	1, 2, 3	sylanbrc 645	1 ⊢ (∀x(x = y → φ) → [y / x]φ)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by:  stdpc4  2024  equsb1  2034  equsb2  2035  sbied  2036  sb6f  2039  hbsb2a  2041  hbsb2e  2042  sb3  2052  sb4b  2054  dfsb2  2055  hbsb2  2057  sbn  2062  sbi1  2063  sb6rf  2091  sbal1  2126  iota4  4358