Theorem wl-2sb6d 38491

Description: Version of 2sb6 2122 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)

Hypotheses

Ref	Expression
wl-2sb6d.1	⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)
wl-2sb6d.2	⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)
wl-2sb6d.3	⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)
wl-2sb6d.4	⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)

Assertion

Ref	Expression
wl-2sb6d	⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))

Proof of Theorem wl-2sb6d

Step	Hyp	Ref	Expression
1		wl-2sb6d.4	. 2 ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)
2		wl-2sb6d.2	. 2 ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)
3		wl-2sb6d.1	. . 3 ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)
4		wl-2sb6d.3	. . 3 ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)
5	3, 4	jca 521	. 2 ⊢ (𝜑 → (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
6		sb4b 2504	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥(𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓)))
7		nfnae 2463	. . . . 5 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑤
8		wl-nfnae1 38461	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑥
9		nfnae 2463	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑧
10	8, 9	nfan 1931	. . . . 5 ⊢ Ⅎ𝑥(¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
11	7, 10	nfan 1931	. . . 4 ⊢ Ⅎ𝑥(¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
12		sb4b 2504	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑤 → ([𝑤 / 𝑦]𝜓 ↔ ∀𝑦(𝑦 = 𝑤 → 𝜓)))
13	12	imbi2d 343	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑤 → ((𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓) ↔ (𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜓))))
14		impexp 456	. . . . . . 7 ⊢ (((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓) ↔ (𝑥 = 𝑧 → (𝑦 = 𝑤 → 𝜓)))
15	14	albii 1851	. . . . . 6 ⊢ (∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓) ↔ ∀𝑦(𝑥 = 𝑧 → (𝑦 = 𝑤 → 𝜓)))
16		nfeqf 2410	. . . . . . 7 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑥 = 𝑧)
17		19.21t 2242	. . . . . . 7 ⊢ (Ⅎ𝑦 𝑥 = 𝑧 → (∀𝑦(𝑥 = 𝑧 → (𝑦 = 𝑤 → 𝜓)) ↔ (𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜓))))
18	16, 17	syl 18	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑦(𝑥 = 𝑧 → (𝑦 = 𝑤 → 𝜓)) ↔ (𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜓))))
19	15, 18	bitr2id 287	. . . . 5 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ((𝑥 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜓)) ↔ ∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
20	13, 19	sylan9bb 519	. . . 4 ⊢ ((¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧)) → ((𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓) ↔ ∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
21	11, 20	albid 2258	. . 3 ⊢ ((¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧)) → (∀𝑥(𝑥 = 𝑧 → [𝑤 / 𝑦]𝜓) ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
22	6, 21	sylan9bb 519	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑦 𝑦 = 𝑤 ∧ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧))) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
23	1, 2, 5, 22	syl12anc 850	1 ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  Ⅎwnf 1815  [wsb 2098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099

This theorem is used by:  wl-sbcom2d-lem2  38493