Step | Hyp | Ref
| Expression |
1 | | df-br 5144 |
. . 3
⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
2 | | relxp 5690 |
. . . . . 6
⊢ Rel
({𝑥} × 𝐵) |
3 | 2 | rgenw 3055 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 Rel ({𝑥} × 𝐵) |
4 | | reliun 5812 |
. . . . 5
⊢ (Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∀𝑥 ∈ 𝐴 Rel ({𝑥} × 𝐵)) |
5 | 3, 4 | mpbir 230 |
. . . 4
⊢ Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
6 | 5 | brrelex1i 5728 |
. . 3
⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 → 𝐶 ∈ V) |
7 | 1, 6 | sylbir 234 |
. 2
⊢
(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝐶 ∈ V) |
8 | | elex 3482 |
. . 3
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ V) |
9 | 8 | adantr 479 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) → 𝐶 ∈ V) |
10 | | nfiu1 5025 |
. . . . 5
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
11 | 10 | nfel2 2911 |
. . . 4
⊢
Ⅎ𝑥⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
12 | | nfv 1909 |
. . . . 5
⊢
Ⅎ𝑥 𝐶 ∈ 𝐴 |
13 | | opeliunxp2f.f |
. . . . . 6
⊢
Ⅎ𝑥𝐸 |
14 | 13 | nfel2 2911 |
. . . . 5
⊢
Ⅎ𝑥 𝐷 ∈ 𝐸 |
15 | 12, 14 | nfan 1894 |
. . . 4
⊢
Ⅎ𝑥(𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) |
16 | 11, 15 | nfbi 1898 |
. . 3
⊢
Ⅎ𝑥(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
17 | | opeq1 4869 |
. . . . 5
⊢ (𝑥 = 𝐶 → ⟨𝑥, 𝐷⟩ = ⟨𝐶, 𝐷⟩) |
18 | 17 | eleq1d 2810 |
. . . 4
⊢ (𝑥 = 𝐶 → (⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
19 | | eleq1 2813 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) |
20 | | opeliunxp2f.e |
. . . . . 6
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) |
21 | 20 | eleq2d 2811 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐷 ∈ 𝐵 ↔ 𝐷 ∈ 𝐸)) |
22 | 19, 21 | anbi12d 630 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
23 | 18, 22 | bibi12d 344 |
. . 3
⊢ (𝑥 = 𝐶 → ((⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) ↔ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)))) |
24 | | opeliunxp 5739 |
. . 3
⊢
(⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) |
25 | 16, 23, 24 | vtoclg1f 3549 |
. 2
⊢ (𝐶 ∈ V → (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
26 | 7, 9, 25 | pm5.21nii 377 |
1
⊢
(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |