Theorem aceq1 3552

Description: Equivalence of two versions of the Axiom of Choice ax-ac 1080. The proof uses neither AC nor the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables.

Assertion

Ref	Expression
aceq1	⊢ (∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∃y∀z∀w((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))

Distinct variable group(s):   x,y,z,w,v,u

Proof of Theorem aceq1

Step	Hyp	Ref	Expression
1		pm4.2i 149	. . . . . . 7 ⊢ (w = t → (∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u)))
2	1	cbvralv 1333	. . . . . 6 ⊢ (∀w ∈ h ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∀t ∈ h ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u))
3		eleq1 1149	. . . . . . . . . . 11 ⊢ (v = z → (v ∈ u ↔ z ∈ u))
4	3	anbi2d 468	. . . . . . . . . 10 ⊢ (v = z → ((h ∈ u ∧ v ∈ u) ↔ (h ∈ u ∧ z ∈ u)))
5	4	birexdv 1220	. . . . . . . . 9 ⊢ (v = z → (∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∃u ∈ y (h ∈ u ∧ z ∈ u)))
6	5	cbvreuv 1335	. . . . . . . 8 ⊢ (∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u))
7		pm4.2 148	. . . . . . . 8 ⊢ (∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u) ↔ ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u))
8	6, 7	bitr 151	. . . . . . 7 ⊢ (∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u))
9	8	biral 1223	. . . . . 6 ⊢ (∀t ∈ h ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∀t ∈ h ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u))
10	2, 9	bitr 151	. . . . 5 ⊢ (∀w ∈ h ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∀t ∈ h ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u))
11	10	biral 1223	. . . 4 ⊢ (∀h ∈ x ∀w ∈ h ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u) ↔ ∀h ∈ x ∀t ∈ h ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u))
12		eleq1 1149	. . . . . . . . 9 ⊢ (z = h → (z ∈ u ↔ h ∈ u))
13	12	anbi1d 469	. . . . . . . 8 ⊢ (z = h → ((z ∈ u ∧ v ∈ u) ↔ (h ∈ u ∧ v ∈ u)))
14	13	birexdv 1220	. . . . . . 7 ⊢ (z = h → (∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∃u ∈ y (h ∈ u ∧ v ∈ u)))
15	14	reueqd 1329	. . . . . 6 ⊢ (z = h → (∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u)))
16	15	raleqd 1327	. . . . 5 ⊢ (z = h → (∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∀w ∈ h ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u)))
17	16	cbvralv 1333	. . . 4 ⊢ (∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∀h ∈ x ∀w ∈ h ∃!v ∈ h ∃u ∈ y (h ∈ u ∧ v ∈ u))
18		eleq1 1149	. . . . . . . . 9 ⊢ (w = h → (w ∈ u ↔ h ∈ u))
19	18	anbi1d 469	. . . . . . . 8 ⊢ (w = h → ((w ∈ u ∧ z ∈ u) ↔ (h ∈ u ∧ z ∈ u)))
20	19	birexdv 1220	. . . . . . 7 ⊢ (w = h → (∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∃u ∈ y (h ∈ u ∧ z ∈ u)))
21	20	reueqd 1329	. . . . . 6 ⊢ (w = h → (∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u)))
22	21	raleqd 1327	. . . . 5 ⊢ (w = h → (∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∀t ∈ h ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u)))
23	22	cbvralv 1333	. . . 4 ⊢ (∀w ∈ x ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∀h ∈ x ∀t ∈ h ∃!z ∈ h ∃u ∈ y (h ∈ u ∧ z ∈ u))
24	11, 17, 23	3bitr4 158	. . 3 ⊢ (∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∀w ∈ x ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u))
25	24	biex 733	. 2 ⊢ (∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∃y∀w ∈ x ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u))
26		19.21v 942	. . . . . 6 ⊢ (∀z(w ∈ x → (z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))) ↔ (w ∈ x → ∀z(z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))))
27		impexp 276	. . . . . . . 8 ⊢ (((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ (z ∈ w → (w ∈ x → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))))
28		bi2.04 141	. . . . . . . 8 ⊢ ((z ∈ w → (w ∈ x → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))) ↔ (w ∈ x → (z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))))
29	27, 28	bitr 151	. . . . . . 7 ⊢ (((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ (w ∈ x → (z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))))
30	29	bial 695	. . . . . 6 ⊢ (∀z((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ ∀z(w ∈ x → (z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))))
31		df-eu 1009	. . . . . . . . . . 11 ⊢ (∃!z(z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ ∃x∀z((z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ z = x))
32		df-reu 1207	. . . . . . . . . . 11 ⊢ (∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∃!z(z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)))
33		19.42v 966	. . . . . . . . . . . . . . 15 ⊢ (∃x(z ∈ w ∧ (x ∈ y ∧ (w ∈ x ∧ z ∈ x))) ↔ (z ∈ w ∧ ∃x(x ∈ y ∧ (w ∈ x ∧ z ∈ x))))
34		an42 389	. . . . . . . . . . . . . . . . 17 ⊢ (((z ∈ w ∧ x ∈ y) ∧ (w ∈ x ∧ z ∈ x)) ↔ ((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)))
35		anass 336	. . . . . . . . . . . . . . . . 17 ⊢ (((z ∈ w ∧ x ∈ y) ∧ (w ∈ x ∧ z ∈ x)) ↔ (z ∈ w ∧ (x ∈ y ∧ (w ∈ x ∧ z ∈ x))))
36	34, 35	bitr3 153	. . . . . . . . . . . . . . . 16 ⊢ (((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ (z ∈ w ∧ (x ∈ y ∧ (w ∈ x ∧ z ∈ x))))
37	36	biex 733	. . . . . . . . . . . . . . 15 ⊢ (∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ ∃x(z ∈ w ∧ (x ∈ y ∧ (w ∈ x ∧ z ∈ x))))
38		df-rex 1206	. . . . . . . . . . . . . . . . 17 ⊢ (∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∃u(u ∈ y ∧ (w ∈ u ∧ z ∈ u)))
39		eleq1 1149	. . . . . . . . . . . . . . . . . . 19 ⊢ (u = x → (u ∈ y ↔ x ∈ y))
40		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (u = x → (w ∈ u ↔ w ∈ x))
41		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (u = x → (z ∈ u ↔ z ∈ x))
42	40, 41	anbi12d 476	. . . . . . . . . . . . . . . . . . 19 ⊢ (u = x → ((w ∈ u ∧ z ∈ u) ↔ (w ∈ x ∧ z ∈ x)))
43	39, 42	anbi12d 476	. . . . . . . . . . . . . . . . . 18 ⊢ (u = x → ((u ∈ y ∧ (w ∈ u ∧ z ∈ u)) ↔ (x ∈ y ∧ (w ∈ x ∧ z ∈ x))))
44	43	cbvexv 973	. . . . . . . . . . . . . . . . 17 ⊢ (∃u(u ∈ y ∧ (w ∈ u ∧ z ∈ u)) ↔ ∃x(x ∈ y ∧ (w ∈ x ∧ z ∈ x)))
45	38, 44	bitr 151	. . . . . . . . . . . . . . . 16 ⊢ (∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∃x(x ∈ y ∧ (w ∈ x ∧ z ∈ x)))
46	45	anbi2i 367	. . . . . . . . . . . . . . 15 ⊢ ((z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ (z ∈ w ∧ ∃x(x ∈ y ∧ (w ∈ x ∧ z ∈ x))))
47	33, 37, 46	3bitr4 158	. . . . . . . . . . . . . 14 ⊢ (∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ (z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)))
48	47	bibi1i 461	. . . . . . . . . . . . 13 ⊢ ((∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x) ↔ ((z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ z = x))
49	48	bial 695	. . . . . . . . . . . 12 ⊢ (∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x) ↔ ∀z((z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ z = x))
50	49	biex 733	. . . . . . . . . . 11 ⊢ (∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x) ↔ ∃x∀z((z ∈ w ∧ ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ z = x))
51	31, 32, 50	3bitr4 158	. . . . . . . . . 10 ⊢ (∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))
52	51	imbi2i 160	. . . . . . . . 9 ⊢ ((t ∈ w → ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ (t ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
53	52	bial 695	. . . . . . . 8 ⊢ (∀t(t ∈ w → ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ ∀t(t ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
54		df-ral 1205	. . . . . . . 8 ⊢ (∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∀t(t ∈ w → ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u)))
55		ax-17 925	. . . . . . . . 9 ⊢ ((z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) → ∀t(z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
56		ax-17 925	. . . . . . . . . 10 ⊢ (t ∈ w → ∀z t ∈ w)
57		hba1 698	. . . . . . . . . . 11 ⊢ (∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x) → ∀z∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))
58	57	hbex 701	. . . . . . . . . 10 ⊢ (∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x) → ∀z∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))
59	56, 58	hbim 702	. . . . . . . . 9 ⊢ ((t ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) → ∀z(t ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
60		eleq1 1149	. . . . . . . . . 10 ⊢ (z = t → (z ∈ w ↔ t ∈ w))
61	60	imbi1d 465	. . . . . . . . 9 ⊢ (z = t → ((z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ (t ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))))
62	55, 59, 61	cbval 848	. . . . . . . 8 ⊢ (∀z(z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ ∀t(t ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
63	53, 54, 62	3bitr4 158	. . . . . . 7 ⊢ (∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∀z(z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
64	63	imbi2i 160	. . . . . 6 ⊢ ((w ∈ x → ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u)) ↔ (w ∈ x → ∀z(z ∈ w → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x))))
65	26, 30, 64	3bitr4 158	. . . . 5 ⊢ (∀z((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ (w ∈ x → ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u)))
66	65	bial 695	. . . 4 ⊢ (∀w∀z((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ ∀w(w ∈ x → ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u)))
67		alcom 715	. . . 4 ⊢ (∀z∀w((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)) ↔ ∀w∀z((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
68		df-ral 1205	. . . 4 ⊢ (∀w ∈ x ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∀w(w ∈ x → ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u)))
69	66, 67, 68	3bitr4r 159	. . 3 ⊢ (∀w ∈ x ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∀z∀w((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
70	69	biex 733	. 2 ⊢ (∃y∀w ∈ x ∀t ∈ w ∃!z ∈ w ∃u ∈ y (w ∈ u ∧ z ∈ u) ↔ ∃y∀z∀w((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))
71	25, 70	bitr 151	1 ⊢ (∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∃y∀z∀w((z ∈ w ∧ w ∈ x) → ∃x∀z(∃x((z ∈ w ∧ w ∈ x) ∧ (z ∈ x ∧ x ∈ y)) ↔ z = x)))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803  ∃!weu 1007  ∀wral 1201  ∃wrex 1202  ∃!wreu 1203

This theorem is referenced by:  aceq0 3553

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-reu 1207

metamath.org