| Step | Hyp | Ref
| Expression |
| 1 | | eueq 3714 |
. . 3
⊢ (𝐵 ∈ V ↔ ∃!𝑦 𝑦 = 𝐵) |
| 2 | 1 | ralbii 3093 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ V ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑦 = 𝐵) |
| 3 | | r19.26 3111 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵)) |
| 4 | | df-eu 2569 |
. . . 4
⊢
(∃!𝑦 𝑦 = 𝐵 ↔ (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵)) |
| 5 | 4 | ralbii 3093 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑦 = 𝐵 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵)) |
| 6 | | df-mpt 5226 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
| 7 | 6 | fneq1i 6665 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} Fn 𝐴) |
| 8 | | df-fn 6564 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} Fn 𝐴 ↔ (Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ∧ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴)) |
| 9 | 7, 8 | bitri 275 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ (Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ∧ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴)) |
| 10 | | moanimv 2619 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑦 = 𝐵)) |
| 11 | 10 | albii 1819 |
. . . . . 6
⊢
(∀𝑥∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑦 = 𝐵)) |
| 12 | | funopab 6601 |
. . . . . 6
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) |
| 13 | | df-ral 3062 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 𝑦 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑦 = 𝐵)) |
| 14 | 11, 12, 13 | 3bitr4ri 304 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 𝑦 = 𝐵 ↔ Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}) |
| 15 | | eqcom 2744 |
. . . . . 6
⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} = 𝐴 ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)}) |
| 16 | | dmopab 5926 |
. . . . . . . 8
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} |
| 17 | | 19.42v 1953 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
| 18 | 17 | abbii 2809 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} |
| 19 | 16, 18 | eqtri 2765 |
. . . . . . 7
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} |
| 20 | 19 | eqeq1i 2742 |
. . . . . 6
⊢ (dom
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴 ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} = 𝐴) |
| 21 | | pm4.71 557 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 → ∃𝑦 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))) |
| 22 | 21 | albii 1819 |
. . . . . . 7
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ∃𝑦 𝑦 = 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))) |
| 23 | | df-ral 3062 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 𝑦 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃𝑦 𝑦 = 𝐵)) |
| 24 | | mptfnf.0 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐴 |
| 25 | 24 | eqabf 2935 |
. . . . . . 7
⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))) |
| 26 | 22, 23, 25 | 3bitr4i 303 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 𝑦 = 𝐵 ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)}) |
| 27 | 15, 20, 26 | 3bitr4ri 304 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 𝑦 = 𝐵 ↔ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴) |
| 28 | 14, 27 | anbi12i 628 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 ∃*𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵) ↔ (Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ∧ dom {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴)) |
| 29 | | ancom 460 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 ∃*𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵)) |
| 30 | 9, 28, 29 | 3bitr2i 299 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵)) |
| 31 | 3, 5, 30 | 3bitr4ri 304 |
. 2
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑦 = 𝐵) |
| 32 | 2, 31 | bitr4i 278 |
1
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ V ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |