Step | Hyp | Ref
| Expression |
1 | | df-br 4004 |
. . 3
⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
2 | | relxp 4735 |
. . . . . 6
⊢ Rel
({𝑥} × 𝐵) |
3 | 2 | rgenw 2532 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 Rel ({𝑥} × 𝐵) |
4 | | reliun 4747 |
. . . . 5
⊢ (Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∀𝑥 ∈ 𝐴 Rel ({𝑥} × 𝐵)) |
5 | 3, 4 | mpbir 146 |
. . . 4
⊢ Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
6 | 5 | brrelex1i 4669 |
. . 3
⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 → 𝐶 ∈ V) |
7 | 1, 6 | sylbir 135 |
. 2
⊢
(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝐶 ∈ V) |
8 | | elex 2748 |
. . 3
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ V) |
9 | 8 | adantr 276 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) → 𝐶 ∈ V) |
10 | | nfiu1 3916 |
. . . . 5
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
11 | 10 | nfel2 2332 |
. . . 4
⊢
Ⅎ𝑥⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
12 | | nfv 1528 |
. . . . 5
⊢
Ⅎ𝑥 𝐶 ∈ 𝐴 |
13 | | opeliunxp2f.f |
. . . . . 6
⊢
Ⅎ𝑥𝐸 |
14 | 13 | nfel2 2332 |
. . . . 5
⊢
Ⅎ𝑥 𝐷 ∈ 𝐸 |
15 | 12, 14 | nfan 1565 |
. . . 4
⊢
Ⅎ𝑥(𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) |
16 | 11, 15 | nfbi 1589 |
. . 3
⊢
Ⅎ𝑥(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
17 | | opeq1 3778 |
. . . . 5
⊢ (𝑥 = 𝐶 → ⟨𝑥, 𝐷⟩ = ⟨𝐶, 𝐷⟩) |
18 | 17 | eleq1d 2246 |
. . . 4
⊢ (𝑥 = 𝐶 → (⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
19 | | eleq1 2240 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
20 | | opeliunxp2f.e |
. . . . . 6
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) |
21 | 20 | eleq2d 2247 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐷 ∈ 𝐵 ↔ 𝐷 ∈ 𝐸)) |
22 | 19, 21 | anbi12d 473 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
23 | 18, 22 | bibi12d 235 |
. . 3
⊢ (𝑥 = 𝐶 → ((⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) ↔ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)))) |
24 | | opeliunxp 4681 |
. . 3
⊢
(⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) |
25 | 16, 23, 24 | vtoclg1f 2796 |
. 2
⊢ (𝐶 ∈ V → (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
26 | 7, 9, 25 | pm5.21nii 704 |
1
⊢
(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |