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	|- (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(s):   x,y,z,w,v,u

Proof of Theorem aceq1

Step	Hyp	Ref	Expression
1		pm4.2i 149	. . . . . . 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 1333	. . . . . 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 1149	. . . . . . . . . . 11 |- (v = z -> (v e. u <-> z e. u))
4	3	anbi2d 468	. . . . . . . . . 10 |- (v = z -> ((h e. u /\ v e. u) <-> (h e. u /\ z e. u)))
5	4	birexdv 1220	. . . . . . . . 9 |- (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 1335	. . . . . . . 8 |- (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		pm4.2 148	. . . . . . . 8 |- (E!z e. h E.u e. y (h e. u /\ z e. u) <-> E!z e. h E.u e. y (h e. u /\ z e. u))
8	6, 7	bitr 151	. . . . . . 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))
9	8	biral 1223	. . . . . 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))
10	2, 9	bitr 151	. . . . 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))
11	10	biral 1223	. . . 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))
12		eleq1 1149	. . . . . . . . 9 |- (z = h -> (z e. u <-> h e. u))
13	12	anbi1d 469	. . . . . . . 8 |- (z = h -> ((z e. u /\ v e. u) <-> (h e. u /\ v e. u)))
14	13	birexdv 1220	. . . . . . 7 |- (z = h -> (E.u e. y (z e. u /\ v e. u) <-> E.u e. y (h e. u /\ v e. u)))
15	14	reueqd 1329	. . . . . 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)))
16	15	raleqd 1327	. . . . 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)))
17	16	cbvralv 1333	. . . 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))
18		eleq1 1149	. . . . . . . . 9 |- (w = h -> (w e. u <-> h e. u))
19	18	anbi1d 469	. . . . . . . 8 |- (w = h -> ((w e. u /\ z e. u) <-> (h e. u /\ z e. u)))
20	19	birexdv 1220	. . . . . . 7 |- (w = h -> (E.u e. y (w e. u /\ z e. u) <-> E.u e. y (h e. u /\ z e. u)))
21	20	reueqd 1329	. . . . . 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)))
22	21	raleqd 1327	. . . . 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)))
23	22	cbvralv 1333	. . . 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))
24	11, 17, 23	3bitr4 158	. . 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))
25	24	biex 733	. 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))
26		19.21v 942	. . . . . 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))))
27		impexp 276	. . . . . . . 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))))
28		bi2.04 141	. . . . . . . 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))))
29	27, 28	bitr 151	. . . . . . 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))))
30	29	bial 695	. . . . . 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))))
31		df-eu 1009	. . . . . . . . . . 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))
32		df-reu 1207	. . . . . . . . . . 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)))
33		19.42v 966	. . . . . . . . . . . . . . 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))))
34		an42 389	. . . . . . . . . . . . . . . . 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)))
35		anass 336	. . . . . . . . . . . . . . . . 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))))
36	34, 35	bitr3 153	. . . . . . . . . . . . . . . 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))))
37	36	biex 733	. . . . . . . . . . . . . . 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))))
38		df-rex 1206	. . . . . . . . . . . . . . . . 17 |- (E.u e. y (w e. u /\ z e. u) <-> E.u(u e. y /\ (w e. u /\ z e. u)))
39		eleq1 1149	. . . . . . . . . . . . . . . . . . 19 |- (u = x -> (u e. y <-> x e. y))
40		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 |- (u = x -> (w e. u <-> w e. x))
41		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 |- (u = x -> (z e. u <-> z e. x))
42	40, 41	anbi12d 476	. . . . . . . . . . . . . . . . . . 19 |- (u = x -> ((w e. u /\ z e. u) <-> (w e. x /\ z e. x)))
43	39, 42	anbi12d 476	. . . . . . . . . . . . . . . . . 18 |- (u = x -> ((u e. y /\ (w e. u /\ z e. u)) <-> (x e. y /\ (w e. x /\ z e. x))))
44	43	cbvexv 973	. . . . . . . . . . . . . . . . 17 |- (E.u(u e. y /\ (w e. u /\ z e. u)) <-> E.x(x e. y /\ (w e. x /\ z e. x)))
45	38, 44	bitr 151	. . . . . . . . . . . . . . . 16 |- (E.u e. y (w e. u /\ z e. u) <-> E.x(x e. y /\