Theorem aceq1 8940

Description: Equivalence of two versions of the Axiom of Choice ax-ac 9281. 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 252	. . . . . . 7 ⊢ (𝑤 = 𝑡 → (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
2	1	cbvralv 3171	. . . . . 6 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
3		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
4	3	anbi2d 740	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → ((ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
5	4	rexbidv 3052	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
6	5	cbvreuv 3173	. . . . . . 7 ⊢ (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
7	6	ralbii 2980	. . . . . 6 ⊢ (∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
8	2, 7	bitri 264	. . . . 5 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
9	8	ralbii 2980	. . . 4 ⊢ (∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
10		eleq1 2689	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
11	10	anbi1d 741	. . . . . . . 8 ⊢ (𝑧 = ℎ → ((𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
12	11	rexbidv 3052	. . . . . . 7 ⊢ (𝑧 = ℎ → (∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	12	reueqd 3148	. . . . . 6 ⊢ (𝑧 = ℎ → (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
14	13	raleqbi1dv 3146	. . . . 5 ⊢ (𝑧 = ℎ → (∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
15	14	cbvralv 3171	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
16		eleq1 2689	. . . . . . . . 9 ⊢ (𝑤 = ℎ → (𝑤 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
17	16	anbi1d 741	. . . . . . . 8 ⊢ (𝑤 = ℎ → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
18	17	rexbidv 3052	. . . . . . 7 ⊢ (𝑤 = ℎ → (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
19	18	reueqd 3148	. . . . . 6 ⊢ (𝑤 = ℎ → (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
20	19	raleqbi1dv 3146	. . . . 5 ⊢ (𝑤 = ℎ → (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
21	20	cbvralv 3171	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
22	9, 15, 21	3bitr4i 292	. . 3 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
23	22	exbii 1774	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
24		19.21v 1868	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
25		impexp 462	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
26		bi2.04 376	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
27	25, 26	bitri 264	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
28	27	albii 1747	. . . . . 6 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
29		df-eu 2474	. . . . . . . . . . 11 ⊢ (∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
30		df-reu 2919	. . . . . . . . . . 11 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
31		19.42v 1918	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
32		an42 866	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
33		anass 681	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
34	32, 33	bitr3i 266	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
35	34	exbii 1774	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
36		df-rex 2918	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
37		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
38		elequ2 2004	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑥))
39		elequ2 2004	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑥))
40	38, 39	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
41	37, 40	anbi12d 747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
42	41	cbvexv 2275	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
43	36, 42	bitri 264	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
44	43	anbi2i 730	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
45	31, 35, 44	3bitr4i 292	. . . . . . . . . . . . . 14 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
46	45	bibi1i 328	. . . . . . . . . . . . 13 ⊢ ((∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
47	46	albii 1747	. . . . . . . . . . . 12 ⊢ (∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
48	47	exbii 1774	. . . . . . . . . . 11 ⊢ (∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
49	29, 30, 48	3bitr4i 292	. . . . . . . . . 10 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
50	49	imbi2i 326	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
51	50	albii 1747	. . . . . . . 8 ⊢ (∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
52		df-ral 2917	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
53		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
54		nfv 1843	. . . . . . . . . 10 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑤
55		nfa1 2028	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
56	55	nfex 2154	. . . . . . . . . 10 ⊢ Ⅎ𝑧∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
57	54, 56	nfim 1825	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
58		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤))
59	58	imbi1d 331	. . . . . . . . 9 ⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
60	53, 57, 59	cbval 2271	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
61	51, 52, 60	3bitr4i 292	. . . . . . 7 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
62	61	imbi2i 326	. . . . . 6 ⊢ ((𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
63	24, 28, 62	3bitr4i 292	. . . . 5 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
64	63	albii 1747	. . . 4 ⊢ (∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
65		alcom 2037	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
66		df-ral 2917	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
67	64, 65, 66	3bitr4ri 293	. . 3 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
68	67	exbii 1774	. 2 ⊢ (∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
69	23, 68	bitri 264	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481  ∃wex 1704  ∃!weu 2470  ∀wral 2912  ∃wrex 2913  ∃!wreu 2914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-reu 2919

This theorem is referenced by:  aceq0  8941  dfac1  8956