Theorem aceq1 4701

Description: Equivalence of two versions of the Axiom of Choice ax-ac 4716. 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	|- (E.yA.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> E.yA.zA.w((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)))

Distinct variable group:   x,y,z,w,v,u

Proof of Theorem aceq1

Step	Hyp	Ref	Expression
1		pm4.2i 171	. . . . . . 7 |- (w = t -> (E!v e. h E.u e. y (h e. u /\ v e. u) <-> E!v e. h E.u e. y (h e. u /\ v e. u)))
2	1	cbvralv 1791	. . . . . 6 |- (A.w e. h E!v e. h E.u e. y (h e. u /\ v e. u) <-> A.t e. h E!v e. h E.u e. y (h e. u /\ v e. u))
3		eleq1 1526	. . . . . . . . . 10 |- (v = z -> (v e. u <-> z e. u))
4	3	anbi2d 614	. . . . . . . . 9 |- (v = z -> ((h e. u /\ v e. u) <-> (h e. u /\ z e. u)))
5	4	rexbidv 1656	. . . . . . . 8 |- (v = z -> (E.u e. y (h e. u /\ v e. u) <-> E.u e. y (h e. u /\ z e. u)))
6	5	cbvreuv 1793	. . . . . . 7 |- (E!v e. h E.u e. y (h e. u /\ v e. u) <-> E!z e. h E.u e. y (h e. u /\ z e. u))
7	6	ralbii 1659	. . . . . 6 |- (A.t e. h E!v e. h E.u e. y (h e. u /\ v e. u) <-> A.t e. h E!z e. h E.u e. y (h e. u /\ z e. u))
8	2, 7	bitr 173	. . . . 5 |- (A.w e. h E!v e. h E.u e. y (h e. u /\ v e. u) <-> A.t e. h E!z e. h E.u e. y (h e. u /\ z e. u))
9	8	ralbii 1659	. . . 4 |- (A.h e. x A.w e. h E!v e. h E.u e. y (h e. u /\ v e. u) <-> A.h e. x A.t e. h E!z e. h E.u e. y (h e. u /\ z e. u))
10		eleq1 1526	. . . . . . . . 9 |- (z = h -> (z e. u <-> h e. u))
11	10	anbi1d 615	. . . . . . . 8 |- (z = h -> ((z e. u /\ v e. u) <-> (h e. u /\ v e. u)))
12	11	rexbidv 1656	. . . . . . 7 |- (z = h -> (E.u e. y (z e. u /\ v e. u) <-> E.u e. y (h e. u /\ v e. u)))
13	12	reueqd 1785	. . . . . 6 |- (z = h -> (E!v e. z E.u e. y (z e. u /\ v e. u) <-> E!v e. h E.u e. y (h e. u /\ v e. u)))
14	13	raleqd 1783	. . . . 5 |- (z = h -> (A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> A.w e. h E!v e. h E.u e. y (h e. u /\ v e. u)))
15	14	cbvralv 1791	. . . 4 |- (A.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> A.h e. x A.w e. h E!v e. h E.u e. y (h e. u /\ v e. u))
16		eleq1 1526	. . . . . . . . 9 |- (w = h -> (w e. u <-> h e. u))
17	16	anbi1d 615	. . . . . . . 8 |- (w = h -> ((w e. u /\ z e. u) <-> (h e. u /\ z e. u)))
18	17	rexbidv 1656	. . . . . . 7 |- (w = h -> (E.u e. y (w e. u /\ z e. u) <-> E.u e. y (h e. u /\ z e. u)))
19	18	reueqd 1785	. . . . . 6 |- (w = h -> (E!z e. w E.u e. y (w e. u /\ z e. u) <-> E!z e. h E.u e. y (h e. u /\ z e. u)))
20	19	raleqd 1783	. . . . 5 |- (w = h -> (A.t e. w E!z e. w E.u e. y (w e. u /\ z e. u) <-> A.t e. h E!z e. h E.u e. y (h e. u /\ z e. u)))
21	20	cbvralv 1791	. . . 4 |- (A.w e. x A.t e. w E!z e. w E.u e. y (w e. u /\ z e. u) <-> A.h e. x A.t e. h E!z e. h E.u e. y (h e. u /\ z e. u))
22	9, 15, 21	3bitr4 183	. . 3 |- (A.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> A.w e. x A.t e. w E!z e. w E.u e. y (w e. u /\ z e. u))
23	22	exbii 1047	. 2 |- (E.yA.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> E.yA.w e. x A.t e. w E!z e. w E.u e. y (w e. u /\ z e. u))
24		19.21v 1280	. . . . . 6 |- (A.z(w e. x -> (z e. w -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))) <-> (w e. x -> A.z(z e. w -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))))
25		impexp 347	. . . . . . . 8 |- (((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)) <-> (z e. w -> (w e. x -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))))
26		bi2.04 160	. . . . . . . 8 |- ((z e. w -> (w e. x -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))) <-> (w e. x -> (z e. w -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))))
27	25, 26	bitr 173	. . . . . . 7 |- (((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)) <-> (w e. x -> (z e. w -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))))
28	27	albii 996	. . . . . 6 |- (A.z((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)) <-> A.z(w e. x -> (z e. w -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))))
29		df-eu 1375	. . . . . . . . . . 11 |- (E!z(z e. w /\ E.u e. y (w e. u /\ z e. u)) <-> E.xA.z((z e. w /\ E.u e. y (w e. u /\ z e. u)) <-> z = x))
30		df-reu 1643	. . . . . . . . . . 11 |- (E!z e. w E.u e. y (w e. u /\ z e. u) <-> E!z(z e. w /\ E.u e. y (w e. u /\ z e. u)))
31		19.42v 1303	. . . . . . . . . . . . . . 15 |- (E.x(z e. w /\ (x e. y /\ (w e. x /\ z e. x))) <-> (z e. w /\ E.x(x e. y /\ (w e. x /\ z e. x))))
32		an42 506	. . . . . . . . . . . . . . . . 17 |- (((z e. w /\ x e. y) /\ (w e. x /\ z e. x)) <-> ((z e. w /\ w e. x) /\ (z e. x /\ x e. y)))
33		anass 439	. . . . . . . . . . . . . . . . 17 |- (((z e. w /\ x e. y) /\ (w e. x /\ z e. x)) <-> (z e. w /\ (x e. y /\ (w e. x /\ z e. x))))
34	32, 33	bitr3 175	. . . . . . . . . . . . . . . 16 |- (((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> (z e. w /\ (x e. y /\ (w e. x /\ z e. x))))
35	34	exbii 1047	. . . . . . . . . . . . . . 15 |- (E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> E.x(z e. w /\ (x e. y /\ (w e. x /\ z e. x))))
36		df-rex 1642	. . . . . . . . . . . . . . . . 17 |- (E.u e. y (w e. u /\ z e. u) <-> E.u(u e. y /\ (w e. u /\ z e. u)))
37		eleq1 1526	. . . . . . . . . . . . . . . . . . 19 |- (u = x -> (u e. y <-> x e. y))
38		eleq2 1527	. . . . . . . . . . . . . . . . . . . 20 |- (u = x -> (w e. u <-> w e. x))
39		eleq2 1527	. . . . . . . . . . . . . . . . . . . 20 |- (u = x -> (z e. u <-> z e. x))
40	38, 39	anbi12d 626	. . . . . . . . . . . . . . . . . . 19 |- (u = x -> ((w e. u /\ z e. u) <-> (w e. x /\ z e. x)))
41	37, 40	anbi12d 626	. . . . . . . . . . . . . . . . . 18 |- (u = x -> ((u e. y /\ (w e. u /\ z e. u)) <-> (x e. y /\ (w e. x /\ z e. x))))
42	41	cbvexv 1310	. . . . . . . . . . . . . . . . 17 |- (E.u(u e. y /\ (w e. u /\ z e. u)) <-> E.x(x e. y /\ (w e. x /\ z e. x)))
43	36, 42	bitr 173	. . . . . . . . . . . . . . . 16 |- (E.u e. y (w e. u /\ z e. u) <-> E.x(x e. y /\ (w e. x /\ z e. x)))
44	43	anbi2i 479	. . . . . . . . . . . . . . 15 |- ((z e. w /\ E.u e. y