Proof of Theorem eqvinop
Step | Hyp | Ref
| Expression |
1 | | eqvinop.1 |
. . . . . . . 8
⊢ B ∈
V |
2 | | eqvinop.2 |
. . . . . . . 8
⊢ 𝐶 ∈ V |
3 | 1, 2 | opth2 3968 |
. . . . . . 7
⊢
(〈x, y〉 = 〈B, 𝐶〉 ↔ (x = B ∧ y = 𝐶)) |
4 | 3 | anbi2i 430 |
. . . . . 6
⊢
((A = 〈x, y〉 ∧ 〈x,
y〉 = 〈B, 𝐶〉) ↔ (A = 〈x,
y〉 ∧
(x = B
∧ y =
𝐶))) |
5 | | ancom 253 |
. . . . . 6
⊢
((A = 〈x, y〉 ∧ (x = B ∧ y = 𝐶)) ↔ ((x = B ∧ y = 𝐶) ∧ A =
〈x, y〉)) |
6 | | anass 381 |
. . . . . 6
⊢
(((x = B ∧ y = 𝐶) ∧
A = 〈x, y〉)
↔ (x = B ∧ (y = 𝐶 ∧ A = 〈x,
y〉))) |
7 | 4, 5, 6 | 3bitri 195 |
. . . . 5
⊢
((A = 〈x, y〉 ∧ 〈x,
y〉 = 〈B, 𝐶〉) ↔ (x = B ∧ (y = 𝐶 ∧ A =
〈x, y〉))) |
8 | 7 | exbii 1493 |
. . . 4
⊢ (∃y(A = 〈x,
y〉 ∧
〈x, y〉 = 〈B, 𝐶〉) ↔ ∃y(x = B ∧ (y = 𝐶 ∧ A =
〈x, y〉))) |
9 | | 19.42v 1783 |
. . . 4
⊢ (∃y(x = B ∧ (y = 𝐶 ∧ A =
〈x, y〉)) ↔ (x = B ∧ ∃y(y = 𝐶 ∧ A =
〈x, y〉))) |
10 | | opeq2 3541 |
. . . . . . 7
⊢ (y = 𝐶 → 〈x, y〉 =
〈x, 𝐶〉) |
11 | 10 | eqeq2d 2048 |
. . . . . 6
⊢ (y = 𝐶 → (A = 〈x,
y〉 ↔ A = 〈x,
𝐶〉)) |
12 | 2, 11 | ceqsexv 2587 |
. . . . 5
⊢ (∃y(y = 𝐶 ∧ A = 〈x,
y〉) ↔ A = 〈x,
𝐶〉) |
13 | 12 | anbi2i 430 |
. . . 4
⊢
((x = B ∧ ∃y(y = 𝐶 ∧ A = 〈x,
y〉)) ↔ (x = B ∧ A =
〈x, 𝐶〉)) |
14 | 8, 9, 13 | 3bitri 195 |
. . 3
⊢ (∃y(A = 〈x,
y〉 ∧
〈x, y〉 = 〈B, 𝐶〉) ↔ (x = B ∧ A =
〈x, 𝐶〉)) |
15 | 14 | exbii 1493 |
. 2
⊢ (∃x∃y(A = 〈x,
y〉 ∧
〈x, y〉 = 〈B, 𝐶〉) ↔ ∃x(x = B ∧ A =
〈x, 𝐶〉)) |
16 | | opeq1 3540 |
. . . 4
⊢ (x = B →
〈x, 𝐶〉 = 〈B, 𝐶〉) |
17 | 16 | eqeq2d 2048 |
. . 3
⊢ (x = B →
(A = 〈x, 𝐶〉 ↔ A = 〈B,
𝐶〉)) |
18 | 1, 17 | ceqsexv 2587 |
. 2
⊢ (∃x(x = B ∧ A =
〈x, 𝐶〉) ↔ A = 〈B,
𝐶〉) |
19 | 15, 18 | bitr2i 174 |
1
⊢ (A = 〈B,
𝐶〉 ↔ ∃x∃y(A = 〈x,
y〉 ∧
〈x, y〉 = 〈B, 𝐶〉)) |