Theorem sb6 1911

Description: Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem sb6

Step	Hyp	Ref	Expression
1		sb56 1910	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2	1	anbi2i 457	. 2 ⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
3		df-sb 1787	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
4		ax-4 1534	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜑))
5	4	pm4.71ri 392	. 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
6	2, 3, 5	3bitr4i 212	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1371  ∃wex 1516  [wsb 1786

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

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

This theorem is referenced by:  sb5  1912  sbnv  1913  sbanv  1914  sbi1v  1916  sbi2v  1917  hbs1  1967  2sb6  2013  sbcom2v  2014  sb6a  2017  sb7af  2022  sbalyz  2028  sbal1yz  2030  exsb  2037  sbal2  2049  cbvabw  2329  nfabdw  2368  csbcow  3108