HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem aceq5 5902
Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is similar to the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is Theorem 6M(4) of [Enderton] p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC.
Assertion
Ref Expression
aceq5 |- (A.xE.f(f C_ x /\ f Fn dom x) <-> A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))
Distinct variable group:   x,f,z,y,w,v
Proof of Theorem aceq5
StepHypRef Expression
1 aceq4 5896 . . 3 |- (A.xE.f(f C_ x /\ f Fn dom x) <-> A.xE.f(f Fn x /\ A.w e. x (w =/= (/) -> (f` w) e. w)))
2 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> (f` w) = (f` t))
3 id 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> w = t)
42, 3eleq12d 1965 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = t -> ((f` w) e. w <-> (f` t) e. t))
5 neeq2 2025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> (z =/= w <-> z =/= t))
6 ineq2 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = t -> (z i^i w) = (z i^i t))
76eqeq1d 1892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> ((z i^i w) = (/) <-> (z i^i t) = (/)))
85, 7imbi12d 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = t -> ((z =/= w -> (z i^i w) = (/)) <-> (z =/= t -> (z i^i t) = (/))))
94, 8anbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = t -> (((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) <-> ((f` t) e. t /\ (z =/= t -> (z i^i t) = (/)))))
109rcla4v 2376 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. x -> (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) -> ((f` t) e. t /\ (z =/= t -> (z i^i t) = (/)))))
11 minel 2929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((f` t) e. t /\ (z i^i t) = (/)) -> -. (f` t) e. z)
1211ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` t) e. t -> ((z i^i t) = (/) -> -. (f` t) e. z))
1312imim2d 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f` t) e. t -> ((z =/= t -> (z i^i t) = (/)) -> (z =/= t -> -. (f` t) e. z)))
1413imp 377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) -> (z =/= t -> -. (f` t) e. z))
1514necon4ad 2071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) -> ((f` t) e. z -> z = t))
1615imp 377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ (f` t) e. z) -> z = t)
17 eleq1 1957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f` t) = v -> ((f` t) e. z <-> v e. z))
1817biimpar 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((f` t) = v /\ v e. z) -> (f` t) e. z)
1916, 18sylan2 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> z = t)
20 eqeq2 1893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` t) = v -> ((f` z) = (f` t) <-> (f` z) = v))
21 eqcom 1886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` z) = v <-> v = (f` z))
2220, 21syl6bb 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f` t) = v -> ((f` z) = (f` t) <-> v = (f` z)))
23 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = t -> (f` z) = (f` t))
2422, 23syl5bi 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f` t) = v -> (z = t -> v = (f` z)))
2524ad2antrl 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> (z = t -> v = (f` z)))
2619, 25mpd 29 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> v = (f` z))
2726exp32 408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) -> ((f` t) = v -> (v e. z -> v = (f` z))))
2810, 27syl6com 64 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) -> (t e. x -> ((f` t) = v -> (v e. z -> v = (f` z)))))
2928com14 42 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. z -> (t e. x -> ((f` t) = v -> (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) -> v = (f` z)))))
3029r19.23adv 2215 . . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. z -> (E.t e. x (f` t) = v -> (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) -> v = (f` z))))
31 fvelrnb 4719 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (f Fn x -> (v e. ran f <-> E.t e. x (f` t) = v))
3231biimpac 462 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((v e. ran f /\ f Fn x) -> E.t e. x (f` t) = v)
3330, 32syl5 20 . . . . . . . . . . . . . . . . . . . . . 22 |- (v e. z -> ((v e. ran f /\ f Fn x) -> (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) -> v = (f` z))))
3433exp3a 405 . . . . . . . . . . . . . . . . . . . . 21 |- (v e. z -> (v e. ran f -> (f Fn x -> (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) -> v = (f` z)))))
3534com4t 44 . . . . . . . . . . . . . . . . . . . 20 |- (f Fn x -> (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) -> (v e. z -> (v e. ran f -> v = (f` z)))))
3635imp4b 392 . . . . . . . . . . . . . . . . . . 19 |- ((f Fn x /\ A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/)))) -> ((v e. z /\ v e. ran f) -> v = (f` z)))
37 elin 2786 . . . . . . . . . . . . . . . . . . 19 |- (v e. (z i^i ran f) <-> (v e. z /\ v e. ran f))
3836, 37syl5ib 223 . . . . . . . . . . . . . . . . . 18 |- ((f Fn x /\ A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/)))) -> (v e. (z i^i ran f) -> v = (f` z)))
39 r19.26 2219 . . . . . . . . . . . . . . . . . 18 |- (A.w e. x ((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) <-> (A.w e. x (f` w) e. w /\ A.w e. x (z =/= w -> (z i^i w) = (/))))
4038, 39sylan2br 502 . . . . . . . . . . . . . . . . 17 |- ((f Fn x /\ (A.w e. x (f` w) e. w /\ A.w e. x (z =/= w -> (z i^i w) = (/)))) -> (v e. (z i^i ran f) -> v = (f` z)))
4140anassrs 489 . . . . . . . . . . . . . . . 16 |- (((f Fn x /\ A.w e. x (f` w) e. w) /\ A.w e. x (z =/= w -> (z i^i w) = (/))) -> (v e. (z i^i ran f) -> v = (f` z)))
4241adantlr 429 . . . . . . . . . . . . . . 15 |- ((((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) /\ A.w e. x (z =/= w -> (z i^i w) = (/))) -> (v e. (z i^i ran f) -> v = (f` z)))
43 eleq1 1957 . . . . . . . . . . . . . . . . 17 |- (v = (f` z) -> (v e. (z i^i ran f) <-> (f` z) e. (z i^i ran f)))
44 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = z -> (f` w) = (f` z))
45 id 73 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = z -> w = z)
4644, 45eleq12d 1965 . . . . . . . . . . . . . . . . . . . . . . 23 |- (w = z -> ((f` w) e. w <-> (f` z) e. z))
4746rcla4v 2376 . . . . . . . . . . . . . . . . . . . . . 22 |- (z e. x -> (A.w e. x (f` w) e. w -> (f` z) e. z))
48 fnfvelrn 4786 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((f Fn x /\ z e. x) -> (f` z) e. ran f)
4948expcom 403 . . . . . . . . . . . . . . . . . . . . . 22 |- (z e. x -> (f Fn x -> (f` z) e. ran f))
5047, 49anim12d 617 . . . . . . . . . . . . . . . . . . . . 21 |- (z e. x -> ((A.w e. x (f` w) e. w /\ f Fn x) -> ((f` z) e. z /\ (f` z) e. ran f)))
51 elin 2786 . . . . . . . . . . . . . . . . . . . . 21 |- ((f` z) e. (z i^i ran f) <-> ((f` z) e. z /\ (f` z) e. ran f))
5250, 51syl6ibr 230 . . . . . . . . . . . . . . . . . . . 20 |- (z e. x -> ((A.w e. x (f` w) e. w /\ f Fn x) -> (f` z) e. (z i^i ran f)))
5352exp3a 405 . . . . . . . . . . . . . . . . . . 19 |- (z e. x -> (A.w e. x (f` w) e. w -> (f Fn x -> (f` z) e. (z i^i ran f))))
5453com13 37 . . . . . . . . . . . . . . . . . 18 |- (f Fn x -> (A.w e. x (f` w) e. w -> (z e. x -> (f` z) e. (z i^i ran f))))
5554imp31 389 . . . . . . . . . . . . . . . . 17 |- (((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) -> (f` z) e. (z i^i ran f))
5643, 55syl5cbir 228 . . . . . . . . . . . . . . . 16 |- (((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) -> (v = (f` z) -> v e. (z i^i ran f)))
5756adantr 425 . . . . . . . . . . . . . . 15 |- ((((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) /\ A.w e. x (z =/= w -> (z i^i w) = (/))) -> (v = (f` z) -> v e. (z i^i ran f)))
5842, 57impbid 574 . . . . . . . . . . . . . 14 |- ((((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) /\ A.w e. x (z =/= w -> (z i^i w) = (/))) -> (v e. (z i^i ran f) <-> v = (f` z)))
5958ex 402 . . . . . . . . . . . . 13 |- (((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) -> (A.w e. x (z =/= w -> (z i^i w) = (/)) -> (v e. (z i^i ran f) <-> v = (f` z))))
605919.21adv 1666 . . . . . . . . . . . 12 |- (((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) -> (A.w e. x (z =/= w -> (z i^i w) = (/)) -> A.v(v e. (z i^i ran f) <-> v = (f` z))))
61 fvex 4689 . . . . . . . . . . . . . 14 |- (f` z) e. _V
62 eqeq2 1893 . . . . . . . . . . . . . . . 16 |- (h = (f` z) -> (v = h <-> v = (f` z)))
6362bibi2d 680 . . . . . . . . . . . . . . 15 |- (h = (f` z) -> ((v e. (z i^i ran f) <-> v = h) <-> (v e. (z i^i ran f) <-> v = (f` z))))
6463albidv 1656 . . . . . . . . . . . . . 14 |- (h = (f` z) -> (A.v(v e. (z i^i ran f) <-> v = h) <-> A.v(v e. (z i^i ran f) <-> v = (f` z))))
6561, 64cla4ev 2371 . . . . . . . . . . . . 13 |- (A.v(v e. (z i^i ran f) <-> v = (f` z)) -> E.hA.v(v e. (z i^i ran f) <-> v = h))
66 df-eu 1775 . . . . . . . . . . . . 13 |- (E!v v e. (z i^i ran f) <-> E.hA.v(v e. (z i^i ran f) <-> v = h))
6765, 66sylibr 217 . . . . . . . . . . . 12 |- (A.v(v e. (z i^i ran f) <-> v = (f` z)) -> E!v v e. (z i^i ran f))
6860, 67syl6 25 . . . . . . . . . . 11 |- (((f Fn x /\ A.w e. x (f` w) e. w) /\ z e. x) -> (A.w e. x (z =/= w -> (z i^i w) = (/)) -> E!v v e. (z i^i ran f)))
6968ralimdvaa 2171 . . . . . . . . . 10 |- ((f Fn x /\ A.w e. x (f` w) e. w) -> (A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) -> A.z e. x E!v v e. (z i^i ran f)))
7069ex 402 . . . . . . . . 9 |- (f Fn x -> (A.w e. x (f` w) e. w -> (A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) -> A.z e. x E!v v e. (z i^i ran f))))
71 neeq1 2024 . . . . . . . . . . . . 13 |- (z = w -> (z =/= (/) <-> w =/= (/)))
7271cbvralv 2280 . . . . . . . . . . . 12 |- (A.z e. x z =/= (/) <-> A.w e. x w =/= (/))
7372anbi2i 538 . . . . . . . . . . 11 |- ((A.w e. x (w =/= (/) -> (f` w) e. w) /\ A.z e. x z =/= (/)) <-> (A.w e. x (w =/= (/) -> (f` w) e. w) /\ A.w e. x w =/= (/)))
74 r19.26 2219 . . . . . . . . . . 11 |- (A.w e. x ((w =/= (/) -> (f` w) e. w) /\ w =/= (/)) <-> (A.w e. x (w =/= (/) -> (f` w) e. w) /\ A.w e. x w =/= (/)))
7573, 74bitr4i 193 . . . . . . . . . 10 |- ((A.w e. x (w =/= (/) -> (f` w) e. w) /\ A.z e. x z =/= (/)) <-> A.w e. x ((w =/= (/) -> (f` w) e. w) /\ w =/= (/)))
76 pm3.35 386 . . . . . . . . . . . 12 |- ((w =/= (/) /\ (w =/= (/) -> (f` w) e. w)) -> (f` w) e. w)
7776ancoms 484 . . . . . . . . . . 11 |- (((w =/= (/) -> (f` w) e. w) /\ w =/= (/)) -> (f` w) e. w)
7877ralimi 2168 . . . . . . . . . 10 |- (A.w e. x ((w =/= (/) -> (f` w) e. w) /\ w =/= (/)) -> A.w e. x (f` w) e. w)
7975, 78sylbi 216 . . . . . . . . 9 |- ((A.w e. x (w =/= (/) -> (f` w) e. w) /\ A.z e. x z =/= (/)) -> A.w e. x (f` w) e. w)
8070, 79syl5 20 . . . . . . . 8 |- (f Fn x -> ((A.w e. x (w =/= (/) -> (f` w) e. w) /\ A.z e. x z =/= (/)) -> (A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) -> A.z e. x E!v v e. (z i^i ran f))))
8180exp3a 405 . . . . . . 7 |- (f Fn x -> (A.w e. x (w =/= (/) -> (f` w) e. w) -> (A.z e. x z =/= (/) -> (A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/)) -> A.z e. x E!v v e. (z i^i ran f)))))
8281imp4b 392 . . . . . 6 |- ((f Fn x /\ A.w e. x (w =/= (/) -> (f` w) e. w)) -> ((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> A.z e. x E!v v e. (z i^i ran f)))
83 visset 2295 . . . . . . . 8 |- f e. _V
8483rnex 4209 . . . . . . 7 |- ran f e. _V
85 ineq2 2790 . . . . . . . . . 10 |- (y = ran f -> (z i^i y) = (z i^i ran f))
8685eleq2d 1964 . . . . . . . . 9 |- (y = ran f -> (v e. (z i^i y) <-> v e. (z i^i ran f)))
8786eubidv 1779 . . . . . . . 8 |- (y = ran f -> (E!v v e. (z i^i y) <-> E!v v e. (z i^i ran f)))
8887ralbidv 2123 . . . . . . 7 |- (y = ran f -> (A.z e. x E!v v e. (z i^i y) <-> A.z e. x E!v v e. (z i^i ran f)))
8984, 88cla4ev 2371 . . . . . 6 |- (A.z e. x E!v v e. (z i^i ran f) -> E.yA.z e. x E!v v e. (z i^i y))
9082, 89syl6 25 . . . . 5 |- ((f Fn x /\ A.w e. x (w =/= (/) -> (f` w) e. w)) -> ((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))
919019.23aiv 1674 . . . 4 |- (E.f(f Fn x /\ A.w e. x (w =/= (/) -> (f` w) e. w)) -> ((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))
9291alimi 1338 . . 3 |- (A.xE.f(f Fn x /\ A.w e. x (w =/= (/) -> (f` w) e. w)) -> A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))
931, 92sylbi 216 . 2 |- (A.xE.f(f C_ x /\ f Fn dom x) -> A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))
94 eqid 1884 . . . . 5 |- {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))} = {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))}
95 eqid 1884 . . . . 5 |- (U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))} i^i y) = (U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))} i^i y)
96 biid 187 . . . . 5 |- (A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)) <-> A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))
9794, 95, 96aceq5lem5 5901 . . . 4 |- (A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)) -> E.fA.w e. h (w =/= (/) -> (f` w) e. w))
989719.21aiv 1664 . . 3 |- (A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)) -> A.hE.fA.w e. h (w =/= (/) -> (f` w) e. w))
99 aceq3 5895 . . . 4 |- (A.xE.f(f C_ x /\ f Fn dom x) <-> A.xE.fA.w e. x (w =/= (/) -> (f` w) e. w))
100 raleq 2266 . . . . . 6 |- (x = h -> (A.w e. x (w =/= (/) -> (f` w) e. w) <-> A.w e. h (w =/= (/) -> (f` w) e. w)))
101100exbidv 1657 . . . . 5 |- (x = h -> (E.fA.w e. x (w =/= (/) -> (f` w) e. w) <-> E.fA.w e. h (w =/= (/) -> (f` w) e. w)))
102101cbvalv 1696 . . . 4 |- (A.xE.fA.w e. x (w =/= (/) -> (f` w) e. w) <-> A.hE.fA.w e. h (w =/= (/) -> (f` w) e. w))
10399, 102bitr2i 191 . . 3 |- (A.hE.fA.w e. h (w =/= (/) -> (f` w) e. w) <-> A.xE.f(f C_ x /\ f Fn dom x))
10498, 103sylib 215 . 2 |- (A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)) -> A.xE.f(f C_ x /\ f Fn dom x))
10593, 104impbii 174 1 |- (A.xE.f(f C_ x /\ f Fn dom x) <-> A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177   X. cxp 3984  dom cdm 3986  ran crn 3987   Fn wfn 3993  ` cfv 3998
This theorem is referenced by:  ac8 5925  aceqkm 5943
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
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-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-id 3586  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