Theorem aceq1 10177

Description: Equivalence of two versions of the Axiom of Choice ax-ac 10518. The proof uses neither AC nor the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by NM, 5-Apr-2004.)

Assertion

Ref	Expression
aceq1	⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢

Proof of Theorem aceq1

Dummy variables 𝑡 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		biidd 265	. . . . . . 7 ⊢ (𝑤 = 𝑡 → (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
2	1	cbvralvw 3241	. . . . . 6 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
3		elequ1 2152	. . . . . . . . . 10 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
4	3	anbi2d 642	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → ((ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
5	4	rexbidv 3187	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
6	5	cbvreuvw 3388	. . . . . . 7 ⊢ (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
7	6	ralbii 3109	. . . . . 6 ⊢ (∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
8	2, 7	bitri 278	. . . . 5 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
9	8	ralbii 3109	. . . 4 ⊢ (∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
10		elequ1 2152	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
11	10	anbi1d 643	. . . . . . . 8 ⊢ (𝑧 = ℎ → ((𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
12	11	rexbidv 3187	. . . . . . 7 ⊢ (𝑧 = ℎ → (∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	12	reueqd 3400	. . . . . 6 ⊢ (𝑧 = ℎ → (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
14	13	raleqbi1dv 3330	. . . . 5 ⊢ (𝑧 = ℎ → (∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
15	14	cbvralvw 3241	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
16		elequ1 2152	. . . . . . . . 9 ⊢ (𝑤 = ℎ → (𝑤 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
17	16	anbi1d 643	. . . . . . . 8 ⊢ (𝑤 = ℎ → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
18	17	rexbidv 3187	. . . . . . 7 ⊢ (𝑤 = ℎ → (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
19	18	reueqd 3400	. . . . . 6 ⊢ (𝑤 = ℎ → (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
20	19	raleqbi1dv 3330	. . . . 5 ⊢ (𝑤 = ℎ → (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
21	20	cbvralvw 3241	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
22	9, 15, 21	3bitr4i 306	. . 3 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
23	22	exbii 1881	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
24		19.21v 1972	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
25		impexp 456	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
26		bi2.04 392	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
27	25, 26	bitri 278	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
28	27	albii 1852	. . . . . 6 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
29		eu6 2600	. . . . . . . . . . 11 ⊢ (∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
30		df-reu 3367	. . . . . . . . . . 11 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
31		19.42v 1986	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
32		an42 670	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
33		anass 474	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
34	32, 33	bitr3i 280	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
35	34	exbii 1881	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
36		df-rex 3088	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
37		elequ1 2152	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
38		elequ2 2160	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑥))
39		elequ2 2160	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑥))
40	38, 39	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
41	37, 40	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
42	41	cbvexvw 2070	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
43	36, 42	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
44	43	anbi2i 635	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
45	31, 35, 44	3bitr4i 306	. . . . . . . . . . . . . 14 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
46	45	bibi1i 341	. . . . . . . . . . . . 13 ⊢ ((∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
47	46	albii 1852	. . . . . . . . . . . 12 ⊢ (∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
48	47	exbii 1881	. . . . . . . . . . 11 ⊢ (∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
49	29, 30, 48	3bitr4i 306	. . . . . . . . . 10 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
50	49	imbi2i 339	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
51	50	albii 1852	. . . . . . . 8 ⊢ (∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
52		df-ral 3078	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
53		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
54		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑤
55		nfa1 2188	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
56	55	nfex 2355	. . . . . . . . . 10 ⊢ Ⅎ𝑧∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
57	54, 56	nfim 1929	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
58		elequ1 2152	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤))
59	58	imbi1d 344	. . . . . . . . 9 ⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
60	53, 57, 59	cbvalv1 2371	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
61	51, 52, 60	3bitr4i 306	. . . . . . 7 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
62	61	imbi2i 339	. . . . . 6 ⊢ ((𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
63	24, 28, 62	3bitr4i 306	. . . . 5 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
64	63	albii 1852	. . . 4 ⊢ (∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
65		alcom 2196	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
66		df-ral 3078	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
67	64, 65, 66	3bitr4ri 307	. . 3 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
68	67	exbii 1881	. 2 ⊢ (∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
69	23, 68	bitri 278	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812  ∃!weu 2594  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-mo 2565  df-eu 2595  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367

This theorem is used by:  aceq0  10178  dfac1  10194