Step | Hyp | Ref
| Expression |
1 | | df-ac 8939 |
. 2
⊢
(CHOICE ↔ ∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
2 | | vex 3203 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
3 | | vuniex 6954 |
. . . . . . . 8
⊢ ∪ 𝑥
∈ V |
4 | 2, 3 | xpex 6962 |
. . . . . . 7
⊢ (𝑥 × ∪ 𝑥)
∈ V |
5 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → 𝑤 ∈ 𝑥) |
6 | | elunii 4441 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑣 ∈ ∪ 𝑥) |
7 | 6 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ 𝑥) |
8 | 5, 7 | jca 554 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)) |
9 | 8 | ssopab2i 5003 |
. . . . . . . 8
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)} |
10 | | df-xp 5120 |
. . . . . . . 8
⊢ (𝑥 × ∪ 𝑥) =
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)} |
11 | 9, 10 | sseqtr4i 3638 |
. . . . . . 7
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ⊆ (𝑥 × ∪ 𝑥) |
12 | 4, 11 | ssexi 4803 |
. . . . . 6
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∈ V |
13 | | sseq2 3627 |
. . . . . . . 8
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑓 ⊆ 𝑦 ↔ 𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
14 | | dmeq 5324 |
. . . . . . . . 9
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → dom 𝑦 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
15 | 14 | fneq2d 5982 |
. . . . . . . 8
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑓 Fn dom 𝑦 ↔ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
16 | 13, 15 | anbi12d 747 |
. . . . . . 7
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}))) |
17 | 16 | exbidv 1850 |
. . . . . 6
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}))) |
18 | 12, 17 | spcv 3299 |
. . . . 5
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
19 | | fndm 5990 |
. . . . . . . . . . . . 13
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → dom 𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
20 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑧 ∈ dom 𝑓 ↔ 𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
21 | | dmopab 5335 |
. . . . . . . . . . . . . . . 16
⊢ dom
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} = {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} |
22 | 21 | eleq2i 2693 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ↔ 𝑧 ∈ {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
23 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
24 | | elequ1 1997 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
25 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ 𝑧)) |
26 | 24, 25 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) ↔ (𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧))) |
27 | 26 | exbidv 1850 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → (∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) ↔ ∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧))) |
28 | 23, 27 | elab 3350 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ↔ ∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧)) |
29 | | 19.42v 1918 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ ∃𝑣 𝑣 ∈ 𝑧)) |
30 | | n0 3931 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ≠ ∅ ↔
∃𝑣 𝑣 ∈ 𝑧) |
31 | 30 | anbi2i 730 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ (𝑧 ∈ 𝑥 ∧ ∃𝑣 𝑣 ∈ 𝑧)) |
32 | 29, 31 | bitr4i 267 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) |
33 | 22, 28, 32 | 3bitrri 287 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
34 | 20, 33 | syl6rbbr 279 |
. . . . . . . . . . . . 13
⊢ (dom
𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
35 | 19, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
36 | 35 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
37 | | fnfun 5988 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → Fun 𝑓) |
38 | | funfvima3 6495 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ 𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
39 | 38 | ancoms 469 |
. . . . . . . . . . . 12
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ Fun 𝑓) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
40 | 37, 39 | sylan2 491 |
. . . . . . . . . . 11
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
41 | 36, 40 | sylbid 230 |
. . . . . . . . . 10
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
42 | 41 | imp 445 |
. . . . . . . . 9
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧})) |
43 | | ibar 525 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑥 → (𝑢 ∈ 𝑧 ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧))) |
44 | 43 | abbi2dv 2742 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑥 → 𝑧 = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)}) |
45 | | imasng 5487 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢}) |
46 | 23, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢} |
47 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑢 ∈ V |
48 | | elequ1 1997 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑧 ↔ 𝑢 ∈ 𝑧)) |
49 | 48 | anbi2d 740 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑢 → ((𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧))) |
50 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} |
51 | 23, 47, 26, 49, 50 | brab 4998 |
. . . . . . . . . . . . . 14
⊢ (𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢 ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)) |
52 | 51 | abbii 2739 |
. . . . . . . . . . . . 13
⊢ {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢} = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)} |
53 | 46, 52 | eqtri 2644 |
. . . . . . . . . . . 12
⊢
({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)} |
54 | 44, 53 | syl6reqr 2675 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑥 → ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = 𝑧) |
55 | 54 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑥 → ((𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) ↔ (𝑓‘𝑧) ∈ 𝑧)) |
56 | 55 | ad2antrl 764 |
. . . . . . . . 9
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → ((𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) ↔ (𝑓‘𝑧) ∈ 𝑧)) |
57 | 42, 56 | mpbid 222 |
. . . . . . . 8
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → (𝑓‘𝑧) ∈ 𝑧) |
58 | 57 | exp32 631 |
. . . . . . 7
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
59 | 58 | ralrimiv 2965 |
. . . . . 6
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
60 | 59 | eximi 1762 |
. . . . 5
⊢
(∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
61 | 18, 60 | syl 17 |
. . . 4
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
62 | 61 | alrimiv 1855 |
. . 3
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
63 | | eqid 2622 |
. . . . 5
⊢ (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) = (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) |
64 | 63 | aceq3lem 8943 |
. . . 4
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
65 | 64 | alrimiv 1855 |
. . 3
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
66 | 62, 65 | impbii 199 |
. 2
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
67 | 1, 66 | bitri 264 |
1
⊢
(CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |