Step | Hyp | Ref
| Expression |
1 | | df-br 4016 |
. . 3
⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
2 | | relxp 4747 |
. . . . . 6
⊢ Rel
({𝑥} × 𝐵) |
3 | 2 | rgenw 2542 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 Rel ({𝑥} × 𝐵) |
4 | | reliun 4759 |
. . . . 5
⊢ (Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∀𝑥 ∈ 𝐴 Rel ({𝑥} × 𝐵)) |
5 | 3, 4 | mpbir 146 |
. . . 4
⊢ Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
6 | 5 | brrelex1i 4681 |
. . 3
⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 → 𝐶 ∈ V) |
7 | 1, 6 | sylbir 135 |
. 2
⊢
(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝐶 ∈ V) |
8 | | elex 2760 |
. . 3
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ V) |
9 | 8 | adantr 276 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) → 𝐶 ∈ V) |
10 | | nfcv 2329 |
. . 3
⊢
Ⅎ𝑥𝐶 |
11 | | nfiu1 3928 |
. . . . 5
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
12 | 11 | nfel2 2342 |
. . . 4
⊢
Ⅎ𝑥⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
13 | | nfv 1538 |
. . . 4
⊢
Ⅎ𝑥(𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) |
14 | 12, 13 | nfbi 1599 |
. . 3
⊢
Ⅎ𝑥(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
15 | | opeq1 3790 |
. . . . 5
⊢ (𝑥 = 𝐶 → ⟨𝑥, 𝐷⟩ = ⟨𝐶, 𝐷⟩) |
16 | 15 | eleq1d 2256 |
. . . 4
⊢ (𝑥 = 𝐶 → (⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
17 | | eleq1 2250 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
18 | | opeliunxp2.1 |
. . . . . 6
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) |
19 | 18 | eleq2d 2257 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐷 ∈ 𝐵 ↔ 𝐷 ∈ 𝐸)) |
20 | 17, 19 | anbi12d 473 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
21 | 16, 20 | bibi12d 235 |
. . 3
⊢ (𝑥 = 𝐶 → ((⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) ↔ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)))) |
22 | | opeliunxp 4693 |
. . 3
⊢
(⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) |
23 | 10, 14, 21, 22 | vtoclgf 2807 |
. 2
⊢ (𝐶 ∈ V → (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
24 | 7, 9, 23 | pm5.21nii 705 |
1
⊢
(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |