MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac9 Structured version   Visualization version   GIF version

Theorem dfac9 9985
Description: Equivalence of the axiom of choice with a statement related to ac9 10332; definition AC3 of [Schechter] p. 139. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Assertion
Ref Expression
dfac9 (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
Distinct variable group:   𝑥,𝑓

Proof of Theorem dfac9
Dummy variables 𝑔 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac3 9970 . 2 (CHOICE ↔ ∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
2 vex 3445 . . . . . . 7 𝑓 ∈ V
32rnex 7819 . . . . . 6 ran 𝑓 ∈ V
4 raleq 3305 . . . . . . 7 (𝑠 = ran 𝑓 → (∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
54exbidv 1923 . . . . . 6 (𝑠 = ran 𝑓 → (∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
63, 5spcv 3553 . . . . 5 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
7 df-nel 3047 . . . . . . . . . . . . . . 15 (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓)
87biimpi 215 . . . . . . . . . . . . . 14 (∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓)
98ad2antlr 724 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓)
10 fvelrn 7004 . . . . . . . . . . . . . . . 16 ((Fun 𝑓𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
1110adantlr 712 . . . . . . . . . . . . . . 15 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
12 eleq1 2824 . . . . . . . . . . . . . . 15 ((𝑓𝑥) = ∅ → ((𝑓𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓))
1311, 12syl5ibcom 244 . . . . . . . . . . . . . 14 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓𝑥) = ∅ → ∅ ∈ ran 𝑓))
1413necon3bd 2954 . . . . . . . . . . . . 13 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (¬ ∅ ∈ ran 𝑓 → (𝑓𝑥) ≠ ∅))
159, 14mpd 15 . . . . . . . . . . . 12 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ≠ ∅)
1615adantlr 712 . . . . . . . . . . 11 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ≠ ∅)
17 neeq1 3003 . . . . . . . . . . . . 13 (𝑡 = (𝑓𝑥) → (𝑡 ≠ ∅ ↔ (𝑓𝑥) ≠ ∅))
18 fveq2 6819 . . . . . . . . . . . . . 14 (𝑡 = (𝑓𝑥) → (𝑔𝑡) = (𝑔‘(𝑓𝑥)))
19 id 22 . . . . . . . . . . . . . 14 (𝑡 = (𝑓𝑥) → 𝑡 = (𝑓𝑥))
2018, 19eleq12d 2831 . . . . . . . . . . . . 13 (𝑡 = (𝑓𝑥) → ((𝑔𝑡) ∈ 𝑡 ↔ (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2117, 20imbi12d 344 . . . . . . . . . . . 12 (𝑡 = (𝑓𝑥) → ((𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))))
22 simplr 766 . . . . . . . . . . . 12 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
2310ad4ant14 749 . . . . . . . . . . . 12 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
2421, 22, 23rspcdva 3571 . . . . . . . . . . 11 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓𝑥) ≠ ∅ → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2516, 24mpd 15 . . . . . . . . . 10 ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
2625ralrimiva 3139 . . . . . . . . 9 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
272dmex 7818 . . . . . . . . . 10 dom 𝑓 ∈ V
28 mptelixpg 8786 . . . . . . . . . 10 (dom 𝑓 ∈ V → ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥)))
2927, 28ax-mp 5 . . . . . . . . 9 ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓𝑥)) ∈ (𝑓𝑥))
3026, 29sylibr 233 . . . . . . . 8 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → (𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓𝑥))
3130ne0d 4281 . . . . . . 7 (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅)
3231ex 413 . . . . . 6 ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
3332exlimdv 1935 . . . . 5 ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∃𝑔𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
346, 33syl5com 31 . . . 4 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
3534alrimiv 1929 . . 3 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
36 fnresi 6607 . . . . . . 7 ( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅})
37 fnfun 6579 . . . . . . 7 (( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅}) → Fun ( I ↾ (𝑠 ∖ {∅})))
3836, 37ax-mp 5 . . . . . 6 Fun ( I ↾ (𝑠 ∖ {∅}))
39 neldifsn 4738 . . . . . 6 ¬ ∅ ∈ (𝑠 ∖ {∅})
40 vex 3445 . . . . . . . . 9 𝑠 ∈ V
4140difexi 5269 . . . . . . . 8 (𝑠 ∖ {∅}) ∈ V
42 resiexg 7821 . . . . . . . 8 ((𝑠 ∖ {∅}) ∈ V → ( I ↾ (𝑠 ∖ {∅})) ∈ V)
4341, 42ax-mp 5 . . . . . . 7 ( I ↾ (𝑠 ∖ {∅})) ∈ V
44 funeq 6498 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (Fun 𝑓 ↔ Fun ( I ↾ (𝑠 ∖ {∅}))))
45 rneq 5871 . . . . . . . . . . . . 13 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = ran ( I ↾ (𝑠 ∖ {∅})))
46 rnresi 6007 . . . . . . . . . . . . 13 ran ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
4745, 46eqtrdi 2792 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = (𝑠 ∖ {∅}))
4847eleq2d 2822 . . . . . . . . . . 11 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∈ ran 𝑓 ↔ ∅ ∈ (𝑠 ∖ {∅})))
4948notbid 317 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (¬ ∅ ∈ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
507, 49bitrid 282 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
5144, 50anbi12d 631 . . . . . . . 8 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ↔ (Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅}))))
52 dmeq 5839 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = dom ( I ↾ (𝑠 ∖ {∅})))
53 dmresi 5985 . . . . . . . . . . . 12 dom ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
5452, 53eqtrdi 2792 . . . . . . . . . . 11 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = (𝑠 ∖ {∅}))
5554ixpeq1d 8760 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓𝑥))
56 fveq1 6818 . . . . . . . . . . . 12 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (𝑓𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥))
57 fvresi 7095 . . . . . . . . . . . 12 (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾ (𝑠 ∖ {∅}))‘𝑥) = 𝑥)
5856, 57sylan9eq 2796 . . . . . . . . . . 11 ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓𝑥) = 𝑥)
5958ixpeq2dva 8763 . . . . . . . . . 10 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
6055, 59eqtrd 2776 . . . . . . . . 9 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
6160neeq1d 3000 . . . . . . . 8 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅ ↔ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
6251, 61imbi12d 344 . . . . . . 7 (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) ↔ ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)))
6343, 62spcv 3553 . . . . . 6 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
6438, 39, 63mp2ani 695 . . . . 5 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)
65 n0 4292 . . . . . 6 (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ ↔ ∃𝑔 𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
66 vex 3445 . . . . . . . . 9 𝑔 ∈ V
6766elixp 8755 . . . . . . . 8 (𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥))
68 eldifsn 4733 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥𝑠𝑥 ≠ ∅))
6968imbi1i 349 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔𝑥) ∈ 𝑥) ↔ ((𝑥𝑠𝑥 ≠ ∅) → (𝑔𝑥) ∈ 𝑥))
70 impexp 451 . . . . . . . . . . . 12 (((𝑥𝑠𝑥 ≠ ∅) → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥𝑠 → (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
7169, 70bitri 274 . . . . . . . . . . 11 ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔𝑥) ∈ 𝑥) ↔ (𝑥𝑠 → (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥)))
7271ralbii2 3088 . . . . . . . . . 10 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 ↔ ∀𝑥𝑠 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥))
73 neeq1 3003 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅))
74 fveq2 6819 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
75 id 22 . . . . . . . . . . . . 13 (𝑥 = 𝑡𝑥 = 𝑡)
7674, 75eleq12d 2831 . . . . . . . . . . . 12 (𝑥 = 𝑡 → ((𝑔𝑥) ∈ 𝑥 ↔ (𝑔𝑡) ∈ 𝑡))
7773, 76imbi12d 344 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡)))
7877cbvralvw 3221 . . . . . . . . . 10 (∀𝑥𝑠 (𝑥 ≠ ∅ → (𝑔𝑥) ∈ 𝑥) ↔ ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
7972, 78bitri 274 . . . . . . . . 9 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 ↔ ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8079biimpi 215 . . . . . . . 8 (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔𝑥) ∈ 𝑥 → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8167, 80simplbiim 505 . . . . . . 7 (𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∀𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8281eximi 1836 . . . . . 6 (∃𝑔 𝑔X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8365, 82sylbi 216 . . . . 5 (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8464, 83syl 17 . . . 4 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ∃𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8584alrimiv 1929 . . 3 (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅) → ∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡))
8635, 85impbii 208 . 2 (∀𝑠𝑔𝑡𝑠 (𝑡 ≠ ∅ → (𝑔𝑡) ∈ 𝑡) ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
871, 86bitri 274 1 (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓𝑥) ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wal 1538   = wceq 1540  wex 1780  wcel 2105  wne 2940  wnel 3046  wral 3061  Vcvv 3441  cdif 3894  c0 4268  {csn 4572  cmpt 5172   I cid 5511  dom cdm 5614  ran crn 5615  cres 5616  Fun wfun 6467   Fn wfn 6468  cfv 6473  Xcixp 8748  CHOICEwac 9964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-ixp 8749  df-ac 9965
This theorem is referenced by:  dfac14  22867  dfac21  41142
  Copyright terms: Public domain W3C validator