Theorem aceq1 9543

Description: Equivalence of two versions of the Axiom of Choice ax-ac 9881. 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 264	. . . . . . 7 ⊢ (𝑤 = 𝑡 → (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
2	1	cbvralvw 3449	. . . . . 6 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
3		elequ1 2121	. . . . . . . . . 10 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
4	3	anbi2d 630	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → ((ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
5	4	rexbidv 3297	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
6	5	cbvreuvw 3451	. . . . . . 7 ⊢ (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
7	6	ralbii 3165	. . . . . 6 ⊢ (∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
8	2, 7	bitri 277	. . . . 5 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
9	8	ralbii 3165	. . . 4 ⊢ (∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
10		elequ1 2121	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
11	10	anbi1d 631	. . . . . . . 8 ⊢ (𝑧 = ℎ → ((𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
12	11	rexbidv 3297	. . . . . . 7 ⊢ (𝑧 = ℎ → (∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	12	reueqd 3419	. . . . . 6 ⊢ (𝑧 = ℎ → (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
14	13	raleqbi1dv 3403	. . . . 5 ⊢ (𝑧 = ℎ → (∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
15	14	cbvralvw 3449	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
16		elequ1 2121	. . . . . . . . 9 ⊢ (𝑤 = ℎ → (𝑤 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
17	16	anbi1d 631	. . . . . . . 8 ⊢ (𝑤 = ℎ → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
18	17	rexbidv 3297	. . . . . . 7 ⊢ (𝑤 = ℎ → (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
19	18	reueqd 3419	. . . . . 6 ⊢ (𝑤 = ℎ → (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
20	19	raleqbi1dv 3403	. . . . 5 ⊢ (𝑤 = ℎ → (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
21	20	cbvralvw 3449	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
22	9, 15, 21	3bitr4i 305	. . 3 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
23	22	exbii 1848	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
24		19.21v 1940	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
25		impexp 453	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
26		bi2.04 391	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
27	25, 26	bitri 277	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
28	27	albii 1820	. . . . . 6 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
29		eu6 2659	. . . . . . . . . . 11 ⊢ (∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
30		df-reu 3145	. . . . . . . . . . 11 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
31		19.42v 1954	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
32		an42 655	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
33		anass 471	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
34	32, 33	bitr3i 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
35	34	exbii 1848	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
36		df-rex 3144	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
37		elequ1 2121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
38		elequ2 2129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑥))
39		elequ2 2129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑥))
40	38, 39	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
41	37, 40	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
42	41	cbvexvw 2044	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
43	36, 42	bitri 277	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
44	43	anbi2i 624	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
45	31, 35, 44	3bitr4i 305	. . . . . . . . . . . . . 14 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
46	45	bibi1i 341	. . . . . . . . . . . . 13 ⊢ ((∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
47	46	albii 1820	. . . . . . . . . . . 12 ⊢ (∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
48	47	exbii 1848	. . . . . . . . . . 11 ⊢ (∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
49	29, 30, 48	3bitr4i 305	. . . . . . . . . 10 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
50	49	imbi2i 338	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
51	50	albii 1820	. . . . . . . 8 ⊢ (∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
52		df-ral 3143	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
53		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
54		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑤
55		nfa1 2155	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
56	55	nfex 2343	. . . . . . . . . 10 ⊢ Ⅎ𝑧∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
57	54, 56	nfim 1897	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
58		elequ1 2121	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤))
59	58	imbi1d 344	. . . . . . . . 9 ⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
60	53, 57, 59	cbvalv1 2361	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
61	51, 52, 60	3bitr4i 305	. . . . . . 7 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
62	61	imbi2i 338	. . . . . 6 ⊢ ((𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
63	24, 28, 62	3bitr4i 305	. . . . 5 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
64	63	albii 1820	. . . 4 ⊢ (∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
65		alcom 2163	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
66		df-ral 3143	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
67	64, 65, 66	3bitr4ri 306	. . 3 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
68	67	exbii 1848	. 2 ⊢ (∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
69	23, 68	bitri 277	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535  ∃wex 1780  ∃!weu 2653  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144  df-reu 3145

This theorem is referenced by:  aceq0  9544  dfac1  9560