Theorem dfsb2 2055

Description: An alternate definition of proper substitution that, like df-sb 1649, mixes free and bound variables to avoid distinct variable requirements. (Contributed by NM, 17-Feb-2005.)

Assertion

Ref	Expression
dfsb2	⊢ ([y / x]φ ↔ ((x = y ∧ φ) ∨ ∀x(x = y → φ)))

Proof of Theorem dfsb2

Step	Hyp	Ref	Expression
1		sp 1747	. . . 4 ⊢ (∀x x = y → x = y)
2		sbequ2 1650	. . . . 5 ⊢ (x = y → ([y / x]φ → φ))
3	2	sps 1754	. . . 4 ⊢ (∀x x = y → ([y / x]φ → φ))
4		orc 374	. . . 4 ⊢ ((x = y ∧ φ) → ((x = y ∧ φ) ∨ ∀x(x = y → φ)))
5	1, 3, 4	ee12an 1363	. . 3 ⊢ (∀x x = y → ([y / x]φ → ((x = y ∧ φ) ∨ ∀x(x = y → φ))))
6		sb4 2053	. . . 4 ⊢ (¬ ∀x x = y → ([y / x]φ → ∀x(x = y → φ)))
7		olc 373	. . . 4 ⊢ (∀x(x = y → φ) → ((x = y ∧ φ) ∨ ∀x(x = y → φ)))
8	6, 7	syl6 29	. . 3 ⊢ (¬ ∀x x = y → ([y / x]φ → ((x = y ∧ φ) ∨ ∀x(x = y → φ))))
9	5, 8	pm2.61i 156	. 2 ⊢ ([y / x]φ → ((x = y ∧ φ) ∨ ∀x(x = y → φ)))
10		sbequ1 1918	. . . 4 ⊢ (x = y → (φ → [y / x]φ))
11	10	imp 418	. . 3 ⊢ ((x = y ∧ φ) → [y / x]φ)
12		sb2 2023	. . 3 ⊢ (∀x(x = y → φ) → [y / x]φ)
13	11, 12	jaoi 368	. 2 ⊢ (((x = y ∧ φ) ∨ ∀x(x = y → φ)) → [y / x]φ)
14	9, 13	impbii 180	1 ⊢ ([y / x]φ ↔ ((x = y ∧ φ) ∨ ∀x(x = y → φ)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∀wal 1540  [wsb 1648

This proof depends on 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 proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is used by:  dfsb3  2056