Step | Hyp | Ref
| Expression |
1 | | risset 3224 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐵 𝑦 = 𝑥) |
2 | 1 | anbi2ci 626 |
. . . 4
⊢ ((𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨𝑥, 𝑥⟩) ↔ (𝐶 = ⟨𝑥, 𝑥⟩ ∧ ∃𝑦 ∈ 𝐵 𝑦 = 𝑥)) |
3 | | r19.42v 3188 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 (𝐶 = ⟨𝑥, 𝑥⟩ ∧ 𝑦 = 𝑥) ↔ (𝐶 = ⟨𝑥, 𝑥⟩ ∧ ∃𝑦 ∈ 𝐵 𝑦 = 𝑥)) |
4 | | opeq2 4836 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑥⟩ = ⟨𝑥, 𝑦⟩) |
5 | 4 | equcoms 2024 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ⟨𝑥, 𝑥⟩ = ⟨𝑥, 𝑦⟩) |
6 | 5 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝐶 = ⟨𝑥, 𝑥⟩ ↔ 𝐶 = ⟨𝑥, 𝑦⟩)) |
7 | 6 | pm5.32ri 577 |
. . . . . 6
⊢ ((𝐶 = ⟨𝑥, 𝑥⟩ ∧ 𝑦 = 𝑥) ↔ (𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝑦 = 𝑥)) |
8 | | vex 3452 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
9 | 8 | ideq 5813 |
. . . . . . . 8
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
10 | | df-br 5111 |
. . . . . . . 8
⊢ (𝑥 I 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ I ) |
11 | | equcom 2022 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
12 | 9, 10, 11 | 3bitr3i 301 |
. . . . . . 7
⊢
(⟨𝑥, 𝑦⟩ ∈ I ↔ 𝑦 = 𝑥) |
13 | 12 | anbi2i 624 |
. . . . . 6
⊢ ((𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ I ) ↔ (𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝑦 = 𝑥)) |
14 | 7, 13 | bitr4i 278 |
. . . . 5
⊢ ((𝐶 = ⟨𝑥, 𝑥⟩ ∧ 𝑦 = 𝑥) ↔ (𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ I )) |
15 | 14 | rexbii 3098 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 (𝐶 = ⟨𝑥, 𝑥⟩ ∧ 𝑦 = 𝑥) ↔ ∃𝑦 ∈ 𝐵 (𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ I )) |
16 | 2, 3, 15 | 3bitr2i 299 |
. . 3
⊢ ((𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨𝑥, 𝑥⟩) ↔ ∃𝑦 ∈ 𝐵 (𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ I )) |
17 | 16 | rexbii 3098 |
. 2
⊢
(∃𝑥 ∈
𝐴 (𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨𝑥, 𝑥⟩) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ I )) |
18 | | rexin 4204 |
. 2
⊢
(∃𝑥 ∈
(𝐴 ∩ 𝐵)𝐶 = ⟨𝑥, 𝑥⟩ ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨𝑥, 𝑥⟩)) |
19 | | elinxp 5980 |
. 2
⊢ (𝐶 ∈ ( I ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐶 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ I )) |
20 | 17, 18, 19 | 3bitr4ri 304 |
1
⊢ (𝐶 ∈ ( I ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)𝐶 = ⟨𝑥, 𝑥⟩) |