| Step | Hyp | Ref
| Expression |
| 1 | | df-ac 10156 |
. 2
⊢
(CHOICE ↔ ∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
| 2 | | vex 3484 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
| 3 | | vuniex 7759 |
. . . . . . . 8
⊢ ∪ 𝑥
∈ V |
| 4 | 2, 3 | xpex 7773 |
. . . . . . 7
⊢ (𝑥 × ∪ 𝑥)
∈ V |
| 5 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → 𝑤 ∈ 𝑥) |
| 6 | | elunii 4912 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑣 ∈ ∪ 𝑥) |
| 7 | 6 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → 𝑣 ∈ ∪ 𝑥) |
| 8 | 5, 7 | jca 511 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) → (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)) |
| 9 | 8 | ssopab2i 5555 |
. . . . . . . 8
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)} |
| 10 | | df-xp 5691 |
. . . . . . . 8
⊢ (𝑥 × ∪ 𝑥) =
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ ∪ 𝑥)} |
| 11 | 9, 10 | sseqtrri 4033 |
. . . . . . 7
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ⊆ (𝑥 × ∪ 𝑥) |
| 12 | 4, 11 | ssexi 5322 |
. . . . . 6
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∈ V |
| 13 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑓 ⊆ 𝑦 ↔ 𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
| 14 | | dmeq 5914 |
. . . . . . . . 9
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → dom 𝑦 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
| 15 | 14 | fneq2d 6662 |
. . . . . . . 8
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑓 Fn dom 𝑦 ↔ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
| 16 | 13, 15 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}))) |
| 17 | 16 | exbidv 1921 |
. . . . . 6
⊢ (𝑦 = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}))) |
| 18 | 12, 17 | spcv 3605 |
. . . . 5
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
| 19 | | fndm 6671 |
. . . . . . . . . . . . 13
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → dom 𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
| 20 | | dmopab 5926 |
. . . . . . . . . . . . . . . 16
⊢ dom
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} = {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} |
| 21 | 20 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ↔ 𝑧 ∈ {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
| 22 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
| 23 | | elequ1 2115 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
| 24 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ 𝑧)) |
| 25 | 23, 24 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) ↔ (𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧))) |
| 26 | 25 | exbidv 1921 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → (∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤) ↔ ∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧))) |
| 27 | 22, 26 | elab 3679 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {𝑤 ∣ ∃𝑣(𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ↔ ∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧)) |
| 28 | | 19.42v 1953 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ ∃𝑣 𝑣 ∈ 𝑧)) |
| 29 | | n0 4353 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ≠ ∅ ↔
∃𝑣 𝑣 ∈ 𝑧) |
| 30 | 29 | anbi2i 623 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ (𝑧 ∈ 𝑥 ∧ ∃𝑣 𝑣 ∈ 𝑧)) |
| 31 | 28, 30 | bitr4i 278 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑣(𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) |
| 32 | 21, 27, 31 | 3bitrri 298 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) |
| 33 | | eleq2 2830 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → (𝑧 ∈ dom 𝑓 ↔ 𝑧 ∈ dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)})) |
| 34 | 32, 33 | bitr4id 290 |
. . . . . . . . . . . . 13
⊢ (dom
𝑓 = dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
| 35 | 19, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) ↔ 𝑧 ∈ dom 𝑓)) |
| 37 | | fnfun 6668 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} → Fun 𝑓) |
| 38 | | funfvima3 7256 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ 𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
| 39 | 38 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ Fun 𝑓) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
| 40 | 37, 39 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ dom 𝑓 → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
| 41 | 36, 40 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}))) |
| 42 | 41 | imp 406 |
. . . . . . . . 9
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → (𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧})) |
| 43 | | imasng 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢}) |
| 44 | 43 | elv 3485 |
. . . . . . . . . . . . 13
⊢
({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢} |
| 45 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑢 ∈ V |
| 46 | | elequ1 2115 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑧 ↔ 𝑢 ∈ 𝑧)) |
| 47 | 46 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑢 → ((𝑧 ∈ 𝑥 ∧ 𝑣 ∈ 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧))) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} = {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} |
| 49 | 22, 45, 25, 47, 48 | brab 5548 |
. . . . . . . . . . . . . 14
⊢ (𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢 ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)) |
| 50 | 49 | abbii 2809 |
. . . . . . . . . . . . 13
⊢ {𝑢 ∣ 𝑧{〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}𝑢} = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)} |
| 51 | 44, 50 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)} |
| 52 | | ibar 528 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑥 → (𝑢 ∈ 𝑧 ↔ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧))) |
| 53 | 52 | eqabdv 2875 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑥 → 𝑧 = {𝑢 ∣ (𝑧 ∈ 𝑥 ∧ 𝑢 ∈ 𝑧)}) |
| 54 | 51, 53 | eqtr4id 2796 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑥 → ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) = 𝑧) |
| 55 | 54 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑥 → ((𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) ↔ (𝑓‘𝑧) ∈ 𝑧)) |
| 56 | 55 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → ((𝑓‘𝑧) ∈ ({〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} “ {𝑧}) ↔ (𝑓‘𝑧) ∈ 𝑧)) |
| 57 | 42, 56 | mpbid 232 |
. . . . . . . 8
⊢ (((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅)) → (𝑓‘𝑧) ∈ 𝑧) |
| 58 | 57 | exp32 420 |
. . . . . . 7
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 59 | 58 | ralrimiv 3145 |
. . . . . 6
⊢ ((𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 60 | 59 | eximi 1835 |
. . . . 5
⊢
(∃𝑓(𝑓 ⊆ {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)} ∧ 𝑓 Fn dom {〈𝑤, 𝑣〉 ∣ (𝑤 ∈ 𝑥 ∧ 𝑣 ∈ 𝑤)}) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 61 | 18, 60 | syl 17 |
. . . 4
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 62 | 61 | alrimiv 1927 |
. . 3
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 63 | | eqid 2737 |
. . . . 5
⊢ (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) = (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢})) |
| 64 | 63 | aceq3lem 10160 |
. . . 4
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
| 65 | 64 | alrimiv 1927 |
. . 3
⊢
(∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦)) |
| 66 | 62, 65 | impbii 209 |
. 2
⊢
(∀𝑦∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 67 | 1, 66 | bitri 275 |
1
⊢
(CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |