Step | Hyp | Ref
| Expression |
1 | | df-ac 9252 |
. 2
⊢
(CHOICE ↔ ∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
2 | | vex 3417 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
3 | | vuniex 7214 |
. . . . . . . 8
⊢ ∪ 𝑥
∈ V |
4 | 2, 3 | xpex 7223 |
. . . . . . 7
⊢ (𝑥 × ∪ 𝑥)
∈ V |
5 | | simpl 476 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → 𝑤 ∈ 𝑥) |
6 | | elunii 4663 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑣 ∈ ∪ 𝑥) |
7 | 6 | ancoms 452 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ 𝑥) |
8 | 5, 7 | jca 507 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)) |
9 | 8 | ssopab2i 5229 |
. . . . . . . 8
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)} |
10 | | df-xp 5348 |
. . . . . . . 8
⊢ (𝑥 × ∪ 𝑥) =
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)} |
11 | 9, 10 | sseqtr4i 3863 |
. . . . . . 7
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ⊆ (𝑥 × ∪ 𝑥) |
12 | 4, 11 | ssexi 5028 |
. . . . . 6
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∈ V |
13 | | sseq2 3852 |
. . . . . . . 8
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑓 ⊆ 𝑦 ↔ 𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
14 | | dmeq 5556 |
. . . . . . . . 9
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → dom 𝑦 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
15 | 14 | fneq2d 6215 |
. . . . . . . 8
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑓 Fn dom 𝑦 ↔ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
16 | 13, 15 | anbi12d 624 |
. . . . . . 7
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}))) |
17 | 16 | exbidv 2020 |
. . . . . 6
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}))) |
18 | 12, 17 | spcv 3516 |
. . . . 5
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
19 | | fndm 6223 |
. . . . . . . . . . . . 13
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → dom 𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
20 | | eleq2 2895 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑧 ∈ dom 𝑓 ↔ 𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
21 | | dmopab 5567 |
. . . . . . . . . . . . . . . 16
⊢ dom
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} = {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} |
22 | 21 | eleq2i 2898 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ↔ 𝑧 ∈ {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
23 | | vex 3417 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
24 | | elequ1 2171 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
25 | | eleq2 2895 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ 𝑧)) |
26 | 24, 25 | anbi12d 624 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) ↔ (𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧))) |
27 | 26 | exbidv 2020 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → (∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) ↔ ∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧))) |
28 | 23, 27 | elab 3571 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ↔ ∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧)) |
29 | | 19.42v 2052 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ ∃𝑣 𝑣 ∈ 𝑧)) |
30 | | n0 4160 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ≠ ∅ ↔
∃𝑣 𝑣 ∈ 𝑧) |
31 | 30 | anbi2i 616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ (𝑧 ∈ 𝑥 ∧ ∃𝑣 𝑣 ∈ 𝑧)) |
32 | 29, 31 | bitr4i 270 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) |
33 | 22, 28, 32 | 3bitrri 290 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
34 | 20, 33 | syl6rbbr 282 |
. . . . . . . . . . . . 13
⊢ (dom
𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
35 | 19, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
36 | 35 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
37 | | fnfun 6221 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → Fun 𝑓) |
38 | | funfvima3 6751 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ 𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
39 | 38 | ancoms 452 |
. . . . . . . . . . . 12
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ Fun 𝑓) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
40 | 37, 39 | sylan2 586 |
. . . . . . . . . . 11
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
41 | 36, 40 | sylbid 232 |
. . . . . . . . . 10
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
42 | 41 | imp 397 |
. . . . . . . . 9
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧})) |
43 | | ibar 524 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑥 → (𝑢 ∈ 𝑧 ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧))) |
44 | 43 | abbi2dv 2947 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑥 → 𝑧 = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)}) |
45 | | imasng 5728 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢}) |
46 | 23, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢} |
47 | | vex 3417 |
. . . . . . . . . . . . . . 15
⊢ 𝑢 ∈ V |
48 | | elequ1 2171 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑧 ↔ 𝑢 ∈ 𝑧)) |
49 | 48 | anbi2d 622 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑢 → ((𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧))) |
50 | | eqid 2825 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} |
51 | 23, 47, 26, 49, 50 | brab 5224 |
. . . . . . . . . . . . . 14
⊢ (𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢 ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)) |
52 | 51 | abbii 2944 |
. . . . . . . . . . . . 13
⊢ {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢} = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)} |
53 | 46, 52 | eqtri 2849 |
. . . . . . . . . . . 12
⊢
({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)} |
54 | 44, 53 | syl6reqr 2880 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑥 → ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = 𝑧) |
55 | 54 | eleq2d 2892 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑥 → ((𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) ↔ (𝑓‘𝑧) ∈ 𝑧)) |
56 | 55 | ad2antrl 719 |
. . . . . . . . 9
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → ((𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) ↔ (𝑓‘𝑧) ∈ 𝑧)) |
57 | 42, 56 | mpbid 224 |
. . . . . . . 8
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → (𝑓‘𝑧) ∈ 𝑧) |
58 | 57 | exp32 413 |
. . . . . . 7
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
59 | 58 | ralrimiv 3174 |
. . . . . 6
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
60 | 59 | eximi 1933 |
. . . . 5
⊢
(∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
61 | 18, 60 | syl 17 |
. . . 4
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
62 | 61 | alrimiv 2026 |
. . 3
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
63 | | eqid 2825 |
. . . . 5
⊢ (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) = (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) |
64 | 63 | aceq3lem 9256 |
. . . 4
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
65 | 64 | alrimiv 2026 |
. . 3
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
66 | 62, 65 | impbii 201 |
. 2
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
67 | 1, 66 | bitri 267 |
1
⊢
(CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |