Theorem aceq6b 5904

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 5909). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 5700 and preleq 5708 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see aceq6a 5903.)

Assertion

Ref	Expression
aceq6b	|- (A.xE.f(f C_ x /\ f Fn dom x) -> A.xE.yA.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)))

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

Proof of Theorem aceq6b

Step	Hyp	Ref	Expression
1		aceq3 5895	. 2 |- (A.xE.f(f C_ x /\ f Fn dom x) <-> A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z))
2		hbra1 2147	. . . . . 6 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> A.zA.z e. x (z =/= (/) -> (f` z) e. z))
3		ra4 2155	. . . . . . . . . . . 12 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (z e. x -> (z =/= (/) -> (f` z) e. z)))
4		fvex 4689	. . . . . . . . . . . . . . 15 |- (f` z) e. _V
5		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (w = (f` z) -> (w e. z <-> (f` z) e. z))
6		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (w = (f` z) -> (w e. v <-> (f` z) e. v))
7	6	anbi2d 678	. . . . . . . . . . . . . . . . 17 |- (w = (f` z) -> ((z e. v /\ w e. v) <-> (z e. v /\ (f` z) e. v)))
8	7	rexbidv 2124	. . . . . . . . . . . . . . . 16 |- (w = (f` z) -> (E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v) <-> E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v)))
9	5, 8	anbi12d 690	. . . . . . . . . . . . . . 15 |- (w = (f` z) -> ((w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) <-> ((f` z) e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v))))
10	4, 9	cla4ev 2371	. . . . . . . . . . . . . 14 |- (((f` z) e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
11		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> (z e. v <-> z e. {(f` z), z}))
12		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> ((f` z) e. v <-> (f` z) e. {(f` z), z}))
13	11, 12	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (v = {(f` z), z} -> ((z e. v /\ (f` z) e. v) <-> (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})))
14	13	rcla4ev 2381	. . . . . . . . . . . . . . 15 |- (({(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} /\ (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})) -> E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v))
15		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- z = z
16		neeq1 2024	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> (u =/= (/) <-> z =/= (/)))
17		eqeq1 1890	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> (u = z <-> z = z))
18	16, 17	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (u = z -> ((u =/= (/) /\ u = z) <-> (z =/= (/) /\ z = z)))
19	18	rcla4ev 2381	. . . . . . . . . . . . . . . . . 18 |- ((z e. x /\ (z =/= (/) /\ z = z)) -> E.u e. x (u =/= (/) /\ u = z))
20	15, 19	mpanr2 776	. . . . . . . . . . . . . . . . 17 |- ((z e. x /\ z =/= (/)) -> E.u e. x (u =/= (/) /\ u = z))
21		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (f` u) = (f` z))
22		preq1 3098	. . . . . . . . . . . . . . . . . . . . 21 |- ((f` u) = (f` z) -> {(f` u), u} = {(f` z), u})
23	21, 22	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> {(f` u), u} = {(f` z), u})
24		preq2 3099	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> {(f` z), u} = {(f` z), z})
25	23, 24	eqtr2d 1926	. . . . . . . . . . . . . . . . . . 19 |- (u = z -> {(f` z), z} = {(f` u), u})
26	25	anim2i 362	. . . . . . . . . . . . . . . . . 18 |- ((u =/= (/) /\ u = z) -> (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
27	26	reximi 2198	. . . . . . . . . . . . . . . . 17 |- (E.u e. x (u =/= (/) /\ u = z) -> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
28	20, 27	syl 12	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ z =/= (/)) -> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
29		prex 3526	. . . . . . . . . . . . . . . . 17 |- {(f` z), z} e. _V
30		eqeq1 1890	. . . . . . . . . . . . . . . . . . 19 |- (g = {(f` z), z} -> (g = {(f` u), u} <-> {(f` z), z} = {(f` u), u}))
31	30	anbi2d 678	. . . . . . . . . . . . . . . . . 18 |- (g = {(f` z), z} -> ((u =/= (/) /\ g = {(f` u), u}) <-> (u =/= (/) /\ {(f` z), z} = {(f` u), u})))
32	31	rexbidv 2124	. . . . . . . . . . . . . . . . 17 |- (g = {(f` z), z} -> (E.u e. x (u =/= (/) /\ g = {(f` u), u}) <-> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u})))
33	29, 32	elab 2403	. . . . . . . . . . . . . . . 16 |- ({(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} <-> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
34	28, 33	sylibr 217	. . . . . . . . . . . . . . 15 |- ((z e. x /\ z =/= (/)) -> {(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})})
35		visset 2295	. . . . . . . . . . . . . . . . 17 |- z e. _V
36	35	prid2 3107	. . . . . . . . . . . . . . . 16 |- z e. {(f` z), z}
37	4	prid1 3106	. . . . . . . . . . . . . . . 16 |- (f` z) e. {(f` z), z}
38	36, 37	pm3.2i 307	. . . . . . . . . . . . . . 15 |- (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})
39	14, 34, 38	sylancl 525	. . . . . . . . . . . . . 14 |- ((z e. x /\ z =/= (/)) -> E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v))
40	10, 39	sylan2 500	. . . . . . . . . . . . 13 |- (((f` z) e. z /\ (z e. x /\ z =/= (/))) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
41	40	ex 402	. . . . . . . . . . . 12 |- ((f` z) e. z -> ((z e. x /\ z =/= (/)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
42	3, 41	syl8 27	. . . . . . . . . . 11 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (z e. x -> (z =/= (/) -> ((z e. x /\ z =/= (/)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))))
43	42	imp3a 388	. . . . . . . . . 10 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. x /\ z =/= (/)) -> ((z e. x /\ z =/= (/)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))))
44	43	pm2.43d 79	. . . . . . . . 9 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. x /\ z =/= (/)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
45		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- v e. _V
46		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . 21 |- (g = v -> (g = {(f` u), u} <-> v = {(f` u), u}))
47	46	anbi2d 678	. . . . . . . . . . . . . . . . . . . 20 |- (g = v -> ((u =/= (/) /\ g = {(f` u), u}) <-> (u =/= (/) /\ v = {(f` u), u})))
48	47	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (g = v -> (E.u e. x (u =/= (/) /\ g = {(f` u), u}) <-> E.u e. x (u =/= (/) /\ v = {(f` u), u})))
49	45, 48	elab 2403	. . . . . . . . . . . . . . . . . 18 |- (v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} <-> E.u e. x (u =/= (/) /\ v = {(f` u), u}))
50		neeq1 2024	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = u -> (z =/= (/) <-> u =/= (/)))
51		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z = u -> (f` z) = (f` u))
52	51	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z = u -> ((f` z) e. z <-> (f` u) e. z))
53		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z = u -> ((f` u) e. z <-> (f` u) e. u))
54	52, 53	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = u -> ((f` z) e. z <-> (f` u) e. u))
55	50, 54	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = u -> ((z =/= (/) -> (f` z) e. z) <-> (u =/= (/) -> (f` u) e. u)))
56	55	rcla4cv 2377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (u e. x -> (u =/= (/) -> (f` u) e. u)))
57		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- w e. _V
58		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f` u) e. _V
59		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- u e. _V
60	57, 35, 58, 59	prel12 3155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (-. w = z -> ({w, z} = {(f` u), u} <-> (w e. {(f` u), u} /\ z e. {(f` u), u})))
61		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = {(f` u), u} -> (w e. v <-> w e. {(f` u), u}))
62		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = {(f` u), u} -> (z e. v <-> z e. {(f` u), u}))
63	61, 62	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = {(f` u), u} -> ((w e. v /\ z e. v) <-> (w e. {(f` u), u} /\ z e. {(f` u), u})))
64		ancom 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((w e. v /\ z e. v) <-> (z e. v /\ w e. v))
65	63, 64	syl5rbbr 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (v = {(f` u), u} -> ((w e. {(f` u), u} /\ z e. {(f` u), u}) <-> (z e. v /\ w e. v)))
66	60, 65	sylan9bbr 600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((v = {(f` u), u} /\ -. w = z) -> ({w, z} = {(f` u), u} <-> (z e. v /\ w e. v)))
67		elirrv 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- -. w e. w
68		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (w = z -> (w e. w <-> w e. z))
69	67, 68	mtbii 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (w = z -> -. w e. z)
70	69	con2i 113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (w e. z -> -. w = z)
71	66, 70	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v = {(f` u), u} /\ w e. z) -> ({w, z} = {(f` u), u} <-> (z e. v /\ w e. v)))
72	71	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((v = {(f` u), u} /\ (w e. z /\ (f` u) e. u)) -> ({w, z} = {(f` u), u} <-> (z e. v /\ w e. v)))
73	72	pm5.32da 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v = {(f` u), u} -> (((w e. z /\ (f` u) e. u) /\ {w, z} = {(f` u), u}) <-> ((w e. z /\ (f` u) e. u) /\ (z e. v /\ w e. v))))
74	57, 35, 58, 59	preleq 5708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((w e. z /\ (f` u) e. u) /\ {w, z} = {(f` u), u}) -> (w = (f` u) /\ z = u))
75	73, 74	syl6bir 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v = {(f` u), u} -> (((w e. z /\ (f` u) e. u) /\ (z e. v /\ w e. v)) -> (w = (f` u) /\ z = u)))
76	51	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z = u -> (w = (f` z) <-> w = (f` u)))
77	76	biimparc 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w = (f` u) /\ z = u) -> w = (f` z))
78	75, 77	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v = {(f` u), u} -> (((w e. z /\ (f` u) e. u) /\ (z e. v /\ w e. v)) -> w = (f` z)))
79	78	exp4c 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = {(f` u), u} -> (w e. z -> ((f` u) e. u -> ((z e. v /\ w e. v) -> w = (f` z)))))
80	79	com13 37	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f` u) e. u -> (w e. z -> (v = {(f` u), u} -> ((z e. v /\ w e. v) -> w = (f` z)))))
81	56, 80	syl8 27	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (u e. x -> (u =/= (/) -> (w e. z -> (v = {(f` u), u} -> ((z e. v /\ w e. v) -> w = (f` z)))))))
82	81	com4r 45	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. z -> (A.z e. x (z =/= (/) -> (f` z) e. z) -> (u e. x -> (u =/= (/) -> (v = {(f` u), u} -> ((z e. v /\ w e. v) -> w = (f` z)))))))
83	82	imp 377	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. z /\ A.z e. x (z =/= (/) -> (f` z) e. z)) -> (u e. x -> (u =/= (/) -> (v = {(f` u), u} -> ((z e. v /\ w e. v) -> w = (f` z))))))
84	83	imp4a 391	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. z /\ A.z e. x (z =/= (/) -> (f` z) e. z)) -> (u e. x -> ((u =/= (/) /\ v = {(f` u), u}) -> ((z e. v /\ w e. v) -> w = (f` z)))))
85	84	com3l 38	. . . . . . . . . . . . . . . . . . 19 |- (u e. x -> ((u =/= (/) /\ v = {(f` u), u}) -> ((w e. z /\ A.z e. x (z =/= (/) -> (f` z) e. z)) -> ((z e. v /\ w e. v) -> w = (f` z)))))
86	85	r19.23aiv 2211	. . . . . . . . . . . . . . . . . 18 |- (E.u e. x (u =/= (/) /\ v = {(f` u), u}) -> ((w e. z /\ A.z e. x (z =/= (/) -> (f` z) e. z)) -> ((z e. v /\ w e. v) -> w = (f` z))))
87	49, 86	sylbi 216	. . . . . . . . . . . . . . . . 17 |- (v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} -> ((w e. z /\ A.z e. x (z =/= (/) -> (f` z) e. z)) -> ((z e. v /\ w e. v) -> w = (f` z))))
88	87	exp3a 405	. . . . . . . . . . . . . . . 16 |- (v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} -> (w e. z -> (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. v /\ w e. v) -> w = (f` z)))))
89	88	com13 37	. . . . . . . . . . . . . . 15 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (w e. z -> (v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} -> ((z e. v /\ w e. v) -> w = (f` z)))))
90	89	imp4b 392	. . . . . . . . . . . . . 14 |- ((A.z e. x (z =/= (/) -> (f` z) e. z) /\ w e. z) -> ((v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} /\ (z e. v /\ w e. v)) -> w = (f` z)))
91	90	19.23adv 1584	. . . . . . . . . . . . 13 |- ((A.z e. x (z =/= (/) -> (f` z) e. z) /\ w e. z) -> (E.v(v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} /\ (z e. v /\ w e. v)) -> w = (f` z)))
92		df-rex 2110	. . . . . . . . . . . . 13 |- (E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v) <-> E.v(v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} /\ (z e. v /\ w e. v)))
93	91, 92	syl5ib 223	. . . . . . . . . . . 12 |- ((A.z e. x (z =/= (/) -> (f` z) e. z) /\ w e. z) -> (E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v) -> w = (f` z)))
94	93	expimpd 404	. . . . . . . . . . 11 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) -> w = (f` z)))
95	94	19.21aiv 1664	. . . . . . . . . 10 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> A.w((w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) -> w = (f` z)))
96		mo2icl 2434	. . . . . . . . . 10 |- (A.w((w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) -> w = (f` z)) -> E*w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
97	95, 96	syl 12	. . . . . . . . 9 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> E*w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
98	44, 97	jctird 663	. . . . . . . 8 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. x /\ z =/= (/)) -> (E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) /\ E*w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))))
99		df-reu 2111	. . . . . . . . 9 |- (E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v) <-> E!w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
100		eu5 1805	. . . . . . . . 9 |- (E!w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) <-> (E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) /\ E*w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
101	99, 100	bitri 190	. . . . . . . 8 |- (E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v) <-> (E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) /\ E*w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
102	98, 101	syl6ibr 230	. . . . . . 7 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. x /\ z =/= (/)) -> E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
103	102	exp3a 405	. . . . . 6 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (z e. x -> (z =/= (/) -> E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
104	2, 103	r19.21ai 2174	. . . . 5 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> A.z e. x (z =/= (/) -> E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
105		visset 2295	. . . . . . . 8 |- x e. _V
106	105	abrexex 4836	. . . . . . 7 |- {g | E.u e. x g = {(f` u), u}} e. _V
107		simpr 350	. . . . . . . . 9 |- ((u =/= (/) /\ g = {(f` u), u}) -> g = {(f` u), u})
108	107	reximi 2198	. . . . . . . 8 |- (E.u e. x (u =/= (/) /\ g = {(f` u), u}) -> E.u e. x g = {(f` u), u})
109	108	ss2abi 2679	. . . . . . 7 |- {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} C_ {g | E.u e. x g = {(f` u), u}}
110	106, 109	ssexi 3456	. . . . . 6 |- {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} e. _V
111		rexeq 2267	. . . . . . . . 9 |- (y = {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} -> (E.v e. y (z e. v /\ w e. v) <-> E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
112	111	reubidv 2260	. . . . . . . 8 |- (y = {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} -> (E!w e. z E.v e. y (z e. v /\ w e. v) <-> E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
113	112	imbi2d 674	. . . . . . 7 |- (y = {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} -> ((z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)) <-> (z =/= (/) -> E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
114	113	ralbidv 2123	. . . . . 6 |- (y = {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} -> (A.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)) <-> A.z e. x (z =/= (/) -> E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
115	110, 114	cla4ev 2371	. . . . 5 |- (A.z e. x (z =/= (/) -> E!w e. z E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) -> E.yA.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)))
116	104, 115	syl 12	. . . 4 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> E.yA.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)))
117	116	19.23aiv 1674	. . 3 |- (E.fA.z e. x (z =/= (/) -> (f` z) e. z) -> E.yA.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)))
118	117	alimi 1338	. 2 |- (A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z) -> A.xE.yA.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)))
119	1, 118	sylbi 216	1 |- (A.xE.f(f C_ x /\ f Fn dom x) -> A.xE.yA.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  E*wmo 1772  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  E!wreu 2107   C_ wss 2593  (/)c0 2875  {cpr 3045  dom cdm 3986   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  aceq7 5905

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-eprel 3583  df-id 3586  df-fr 3625  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014

Copyright terms: Public domain