Theorem aceq1 9857

Description: Equivalence of two versions of the Axiom of Choice ax-ac 10199. 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 261	. . . . . . 7 ⊢ (𝑤 = 𝑡 → (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
2	1	cbvralvw 3380	. . . . . 6 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
3		elequ1 2116	. . . . . . . . . 10 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
4	3	anbi2d 628	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → ((ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
5	4	rexbidv 3227	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
6	5	cbvreuvw 3383	. . . . . . 7 ⊢ (∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
7	6	ralbii 3092	. . . . . 6 ⊢ (∀𝑡 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
8	2, 7	bitri 274	. . . . 5 ⊢ (∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
9	8	ralbii 3092	. . . 4 ⊢ (∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
10		elequ1 2116	. . . . . . . . 9 ⊢ (𝑧 = ℎ → (𝑧 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
11	10	anbi1d 629	. . . . . . . 8 ⊢ (𝑧 = ℎ → ((𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
12	11	rexbidv 3227	. . . . . . 7 ⊢ (𝑧 = ℎ → (∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	12	reueqd 3348	. . . . . 6 ⊢ (𝑧 = ℎ → (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
14	13	raleqbi1dv 3338	. . . . 5 ⊢ (𝑧 = ℎ → (∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
15	14	cbvralvw 3380	. . . 4 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑤 ∈ ℎ ∃!𝑣 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
16		elequ1 2116	. . . . . . . . 9 ⊢ (𝑤 = ℎ → (𝑤 ∈ 𝑢 ↔ ℎ ∈ 𝑢))
17	16	anbi1d 629	. . . . . . . 8 ⊢ (𝑤 = ℎ → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
18	17	rexbidv 3227	. . . . . . 7 ⊢ (𝑤 = ℎ → (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
19	18	reueqd 3348	. . . . . 6 ⊢ (𝑤 = ℎ → (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
20	19	raleqbi1dv 3338	. . . . 5 ⊢ (𝑤 = ℎ → (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
21	20	cbvralvw 3380	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀ℎ ∈ 𝑥 ∀𝑡 ∈ ℎ ∃!𝑧 ∈ ℎ ∃𝑢 ∈ 𝑦 (ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
22	9, 15, 21	3bitr4i 302	. . 3 ⊢ (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
23	22	exbii 1853	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢))
24		19.21v 1945	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
25		impexp 450	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
26		bi2.04 388	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
27	25, 26	bitri 274	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
28	27	albii 1825	. . . . . 6 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤 ∈ 𝑥 → (𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
29		eu6 2575	. . . . . . . . . . 11 ⊢ (∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
30		df-reu 3072	. . . . . . . . . . 11 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃!𝑧(𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
31		19.42v 1960	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
32		an42 653	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
33		anass 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
34	32, 33	bitr3i 276	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
35	34	exbii 1853	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥(𝑧 ∈ 𝑤 ∧ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
36		df-rex 3071	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
37		elequ1 2116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
38		elequ2 2124	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑥))
39		elequ2 2124	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = 𝑥 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑥))
40	38, 39	anbi12d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → ((𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
41	37, 40	anbi12d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
42	41	cbvexvw 2043	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
43	36, 42	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)))
44	43	anbi2i 622	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥))))
45	31, 35, 44	3bitr4i 302	. . . . . . . . . . . . . 14 ⊢ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
46	45	bibi1i 338	. . . . . . . . . . . . 13 ⊢ ((∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
47	46	albii 1825	. . . . . . . . . . . 12 ⊢ (∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
48	47	exbii 1853	. . . . . . . . . . 11 ⊢ (∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥∀𝑧((𝑧 ∈ 𝑤 ∧ ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ 𝑧 = 𝑥))
49	29, 30, 48	3bitr4i 302	. . . . . . . . . 10 ⊢ (∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
50	49	imbi2i 335	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
51	50	albii 1825	. . . . . . . 8 ⊢ (∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
52		df-ral 3070	. . . . . . . 8 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
53		nfv 1920	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
54		nfv 1920	. . . . . . . . . 10 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑤
55		nfa1 2151	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
56	55	nfex 2321	. . . . . . . . . 10 ⊢ Ⅎ𝑧∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)
57	54, 56	nfim 1902	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
58		elequ1 2116	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤))
59	58	imbi1d 341	. . . . . . . . 9 ⊢ (𝑧 = 𝑡 → ((𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
60	53, 57, 59	cbvalv1 2341	. . . . . . . 8 ⊢ (∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
61	51, 52, 60	3bitr4i 302	. . . . . . 7 ⊢ (∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
62	61	imbi2i 335	. . . . . 6 ⊢ ((𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)) ↔ (𝑤 ∈ 𝑥 → ∀𝑧(𝑧 ∈ 𝑤 → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))))
63	24, 28, 62	3bitr4i 302	. . . . 5 ⊢ (∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
64	63	albii 1825	. . . 4 ⊢ (∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
65		alcom 2159	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤∀𝑧((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
66		df-ral 3070	. . . 4 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢)))
67	64, 65, 66	3bitr4ri 303	. . 3 ⊢ (∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
68	67	exbii 1853	. 2 ⊢ (∃𝑦∀𝑤 ∈ 𝑥 ∀𝑡 ∈ 𝑤 ∃!𝑧 ∈ 𝑤 ∃𝑢 ∈ 𝑦 (𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
69	23, 68	bitri 274	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1539  ∃wex 1785  ∃!weu 2569  ∀wral 3065  ∃wrex 3066  ∃!wreu 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-nf 1790  df-mo 2541  df-eu 2570  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-reu 3072

This theorem is referenced by:  aceq0  9858  dfac1  9874