Proof of Theorem dmrab
Step | Hyp | Ref
| Expression |
1 | | dmrab.1 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) |
2 | 1 | elrab 3585 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} ↔ (〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ∧ 𝜓)) |
3 | | opelxp 5555 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
4 | 3 | anbi1i 627 |
. . . . . . . 8
⊢
((〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ∧ 𝜓) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)) |
5 | | ancom 464 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) |
6 | 5 | anbi1i 627 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓)) |
7 | 2, 4, 6 | 3bitri 300 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓)) |
8 | | anass 472 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) ↔ (𝑦 ∈ 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) |
9 | | ancom 464 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝜓 ∧ 𝑥 ∈ 𝐴)) |
10 | 9 | anbi2i 626 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) ↔ (𝑦 ∈ 𝐵 ∧ (𝜓 ∧ 𝑥 ∈ 𝐴))) |
11 | 7, 8, 10 | 3bitri 300 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ (𝜓 ∧ 𝑥 ∈ 𝐴))) |
12 | 11 | exbii 1854 |
. . . . 5
⊢
(∃𝑦〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝜓 ∧ 𝑥 ∈ 𝐴))) |
13 | | df-rex 3059 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 (𝜓 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ (𝜓 ∧ 𝑥 ∈ 𝐴))) |
14 | | r19.41v 3250 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 (𝜓 ∧ 𝑥 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐵 𝜓 ∧ 𝑥 ∈ 𝐴)) |
15 | 12, 13, 14 | 3bitr2i 302 |
. . . 4
⊢
(∃𝑦〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} ↔ (∃𝑦 ∈ 𝐵 𝜓 ∧ 𝑥 ∈ 𝐴)) |
16 | 15 | biancomi 466 |
. . 3
⊢
(∃𝑦〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
17 | 16 | abbii 2803 |
. 2
⊢ {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑}} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜓)} |
18 | | dfdm3 5724 |
. 2
⊢ dom
{𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {𝑥 ∣ ∃𝑦〈𝑥, 𝑦〉 ∈ {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑}} |
19 | | df-rab 3062 |
. 2
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜓)} |
20 | 17, 18, 19 | 3eqtr4i 2771 |
1
⊢ dom
{𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} |