Theorem sb2 1789

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

Assertion

Ref	Expression
sb2	⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)

Proof of Theorem sb2

Step	Hyp	Ref	Expression
1		ax-4 1532	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑))
2		equs4 1747	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
3		df-sb 1785	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
4	1, 2, 3	sylanbrc 417	1 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1370  ∃wex 1514  [wsb 1784

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-i9 1552  ax-ial 1556

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

This theorem is referenced by:  stdpc4  1797  equsb1  1807  equsb2  1808  sbiedh  1809  sb6f  1825  hbsb2a  1828  hbsb2e  1829  sbcof2  1832  sb3  1853  sb4b  1856  sb4bor  1857  hbsb2  1858  nfsb2or  1859  sb6rf  1875  sbi1v  1914  sbalyz  2026  iota4  5248