Theorem aceq1 9731

Description: Equivalence of two versions of the Axiom of Choice ax-ac 10073. 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 3358	. . . . . 6 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
3		elequ1 2117	. . . . . . . . . 10 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
4	3	anbi2d 632	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → ((ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
5	4	rexbidv 3216	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
6	5	cbvreuvw 3361	. . . . . . 7 ⊢ (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
7	6	ralbii 3088	. . . . . 6 ⊢ (∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
8	2, 7	bitri 278	. . . . 5 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
9	8	ralbii 3088	. . . 4 ⊢ (∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
10		elequ1 2117	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
11	10	anbi1d 633	. . . . . . . 8 ⊢ (𝑧 = ℎ → ((𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
12	11	rexbidv 3216	. . . . . . 7 ⊢ (𝑧 = ℎ → (∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	12	reueqd 3327	. . . . . 6 ⊢ (𝑧 = ℎ → (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
14	13	raleqbi1dv 3317	. . . . 5 ⊢ (𝑧 = ℎ → (∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
15	14	cbvralvw 3358	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
16		elequ1 2117	. . . . . . . . 9 ⊢ (𝑤 = ℎ → (𝑤 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
17	16	anbi1d 633	. . . . . . . 8 ⊢ (𝑤 = ℎ → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
18	17	rexbidv 3216	. . . . . . 7 ⊢ (𝑤 = ℎ → (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
19	18	reueqd 3327	. . . . . 6 ⊢ (𝑤 = ℎ → (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
20	19	raleqbi1dv 3317	. . . . 5 ⊢ (𝑤 = ℎ → (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
21	20	cbvralvw 3358	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
22	9, 15, 21	3bitr4i 306	. . 3 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
23	22	exbii 1855	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
24		19.21v 1947	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
25		impexp 454	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
26		bi2.04 392	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
27	25, 26	bitri 278	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
28	27	albii 1827	. . . . . 6 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
29		eu6 2573	. . . . . . . . . . 11 ⊢ (∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
30		df-reu 3068	. . . . . . . . . . 11 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
31		19.42v 1962	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
32		an42 657	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
33		anass 472	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
34	32, 33	bitr3i 280	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
35	34	exbii 1855	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
36		df-rex 3067	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
37		elequ1 2117	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
38		elequ2 2125	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑥))
39		elequ2 2125	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑥))
40	38, 39	anbi12d 634	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
41	37, 40	anbi12d 634	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
42	41	cbvexvw 2045	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
43	36, 42	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
44	43	anbi2i 626	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
45	31, 35, 44	3bitr4i 306	. . . . . . . . . . . . . 14 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
46	45	bibi1i 342	. . . . . . . . . . . . 13 ⊢ ((∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
47	46	albii 1827	. . . . . . . . . . . 12 ⊢ (∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
48	47	exbii 1855	. . . . . . . . . . 11 ⊢ (∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
49	29, 30, 48	3bitr4i 306	. . . . . . . . . 10 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
50	49	imbi2i 339	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
51	50	albii 1827	. . . . . . . 8 ⊢ (∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
52		df-ral 3066	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
53		nfv 1922	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
54		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑤
55		nfa1 2152	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
56	55	nfex 2323	. . . . . . . . . 10 ⊢ Ⅎ𝑧∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
57	54, 56	nfim 1904	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
58		elequ1 2117	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤))
59	58	imbi1d 345	. . . . . . . . 9 ⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
60	53, 57, 59	cbvalv1 2341	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
61	51, 52, 60	3bitr4i 306	. . . . . . 7 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
62	61	imbi2i 339	. . . . . 6 ⊢ ((𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
63	24, 28, 62	3bitr4i 306	. . . . 5 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
64	63	albii 1827	. . . 4 ⊢ (∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
65		alcom 2160	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
66		df-ral 3066	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
67	64, 65, 66	3bitr4ri 307	. . 3 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
68	67	exbii 1855	. 2 ⊢ (∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
69	23, 68	bitri 278	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541  ∃wex 1787  ∃!weu 2567  ∀wral 3061  ∃wrex 3062  ∃!wreu 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-nf 1792  df-mo 2539  df-eu 2568  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-reu 3068

This theorem is referenced by:  aceq0  9732  dfac1  9748