Step | Hyp | Ref
| Expression |
1 | | preq1 3438 |
. . . . . . 7
⊢ (x = A →
{x, y}
= {A, y}) |
2 | 1 | eqeq1d 2045 |
. . . . . 6
⊢ (x = A →
({x, y}
= {z, 𝐷} ↔ {A, y} =
{z, 𝐷})) |
3 | | eqeq1 2043 |
. . . . . . . 8
⊢ (x = A →
(x = z
↔ A = z)) |
4 | 3 | anbi1d 438 |
. . . . . . 7
⊢ (x = A →
((x = z
∧ y =
𝐷) ↔ (A = z ∧ y = 𝐷))) |
5 | | eqeq1 2043 |
. . . . . . . 8
⊢ (x = A →
(x = 𝐷 ↔ A = 𝐷)) |
6 | 5 | anbi1d 438 |
. . . . . . 7
⊢ (x = A →
((x = 𝐷 ∧ y = z) ↔
(A = 𝐷 ∧ y = z))) |
7 | 4, 6 | orbi12d 706 |
. . . . . 6
⊢ (x = A →
(((x = z ∧ y = 𝐷) ∨
(x = 𝐷 ∧ y = z)) ↔
((A = z
∧ y =
𝐷)
∨ (A = 𝐷 ∧ y = z)))) |
8 | 2, 7 | bibi12d 224 |
. . . . 5
⊢ (x = A →
(({x, y} = {z, 𝐷} ↔ ((x = z ∧ y = 𝐷)
∨ (x = 𝐷 ∧ y = z))) ↔
({A, y}
= {z, 𝐷} ↔ ((A = z ∧ y = 𝐷)
∨ (A = 𝐷 ∧ y = z))))) |
9 | 8 | imbi2d 219 |
. . . 4
⊢ (x = A →
((𝐷 ∈ 𝑌 → ({x, y} =
{z, 𝐷} ↔ ((x = z ∧ y = 𝐷)
∨ (x = 𝐷 ∧ y = z)))) ↔
(𝐷 ∈ 𝑌 → ({A, y} =
{z, 𝐷} ↔ ((A = z ∧ y = 𝐷)
∨ (A = 𝐷 ∧ y = z)))))) |
10 | | preq2 3439 |
. . . . . . 7
⊢ (y = B →
{A, y}
= {A, B}) |
11 | 10 | eqeq1d 2045 |
. . . . . 6
⊢ (y = B →
({A, y}
= {z, 𝐷} ↔ {A, B} =
{z, 𝐷})) |
12 | | eqeq1 2043 |
. . . . . . . 8
⊢ (y = B →
(y = 𝐷 ↔ B = 𝐷)) |
13 | 12 | anbi2d 437 |
. . . . . . 7
⊢ (y = B →
((A = z
∧ y =
𝐷) ↔ (A = z ∧ B = 𝐷))) |
14 | | eqeq1 2043 |
. . . . . . . 8
⊢ (y = B →
(y = z
↔ B = z)) |
15 | 14 | anbi2d 437 |
. . . . . . 7
⊢ (y = B →
((A = 𝐷 ∧ y = z) ↔
(A = 𝐷 ∧ B = z))) |
16 | 13, 15 | orbi12d 706 |
. . . . . 6
⊢ (y = B →
(((A = z ∧ y = 𝐷) ∨
(A = 𝐷 ∧ y = z)) ↔
((A = z
∧ B =
𝐷)
∨ (A = 𝐷 ∧ B = z)))) |
17 | 11, 16 | bibi12d 224 |
. . . . 5
⊢ (y = B →
(({A, y} = {z, 𝐷} ↔ ((A = z ∧ y = 𝐷)
∨ (A = 𝐷 ∧ y = z))) ↔
({A, B}
= {z, 𝐷} ↔ ((A = z ∧ B = 𝐷)
∨ (A = 𝐷 ∧ B = z))))) |
18 | 17 | imbi2d 219 |
. . . 4
⊢ (y = B →
((𝐷 ∈ 𝑌 → ({A, y} =
{z, 𝐷} ↔ ((A = z ∧ y = 𝐷)
∨ (A = 𝐷 ∧ y = z)))) ↔
(𝐷 ∈ 𝑌 → ({A, B} =
{z, 𝐷} ↔ ((A = z ∧ B = 𝐷)
∨ (A = 𝐷 ∧ B = z)))))) |
19 | | preq1 3438 |
. . . . . . 7
⊢ (z = 𝐶 → {z, 𝐷} = {𝐶, 𝐷}) |
20 | 19 | eqeq2d 2048 |
. . . . . 6
⊢ (z = 𝐶 → ({A, B} =
{z, 𝐷} ↔ {A, B} = {𝐶, 𝐷})) |
21 | | eqeq2 2046 |
. . . . . . . 8
⊢ (z = 𝐶 → (A = z ↔
A = 𝐶)) |
22 | 21 | anbi1d 438 |
. . . . . . 7
⊢ (z = 𝐶 → ((A = z ∧ B = 𝐷) ↔ (A = 𝐶 ∧ B = 𝐷))) |
23 | | eqeq2 2046 |
. . . . . . . 8
⊢ (z = 𝐶 → (B = z ↔
B = 𝐶)) |
24 | 23 | anbi2d 437 |
. . . . . . 7
⊢ (z = 𝐶 → ((A = 𝐷 ∧ B = z) ↔
(A = 𝐷 ∧ B = 𝐶))) |
25 | 22, 24 | orbi12d 706 |
. . . . . 6
⊢ (z = 𝐶 → (((A = z ∧ B = 𝐷)
∨ (A = 𝐷 ∧ B = z)) ↔
((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶)))) |
26 | 20, 25 | bibi12d 224 |
. . . . 5
⊢ (z = 𝐶 → (({A, B} =
{z, 𝐷} ↔ ((A = z ∧ B = 𝐷)
∨ (A = 𝐷 ∧ B = z))) ↔
({A, B}
= {𝐶, 𝐷} ↔ ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶))))) |
27 | 26 | imbi2d 219 |
. . . 4
⊢ (z = 𝐶 → ((𝐷 ∈ 𝑌 → ({A, B} =
{z, 𝐷} ↔ ((A = z ∧ B = 𝐷)
∨ (A = 𝐷 ∧ B = z)))) ↔
(𝐷 ∈ 𝑌 → ({A, B} = {𝐶, 𝐷} ↔ ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶)))))) |
28 | | preq2 3439 |
. . . . . . 7
⊢ (w = 𝐷 → {z, w} =
{z, 𝐷}) |
29 | 28 | eqeq2d 2048 |
. . . . . 6
⊢ (w = 𝐷 → ({x, y} =
{z, w}
↔ {x, y} = {z, 𝐷})) |
30 | | eqeq2 2046 |
. . . . . . . 8
⊢ (w = 𝐷 → (y = w ↔
y = 𝐷)) |
31 | 30 | anbi2d 437 |
. . . . . . 7
⊢ (w = 𝐷 → ((x = z ∧ y = w) ↔ (x =
z ∧
y = 𝐷))) |
32 | | eqeq2 2046 |
. . . . . . . 8
⊢ (w = 𝐷 → (x = w ↔
x = 𝐷)) |
33 | 32 | anbi1d 438 |
. . . . . . 7
⊢ (w = 𝐷 → ((x = w ∧ y = z) ↔ (x =
𝐷 ∧ y = z))) |
34 | 31, 33 | orbi12d 706 |
. . . . . 6
⊢ (w = 𝐷 → (((x = z ∧ y = w) ∨ (x = w ∧ y = z)) ↔ ((x =
z ∧
y = 𝐷) ∨
(x = 𝐷 ∧ y = z)))) |
35 | | vex 2554 |
. . . . . . 7
⊢ x ∈
V |
36 | | vex 2554 |
. . . . . . 7
⊢ y ∈
V |
37 | | vex 2554 |
. . . . . . 7
⊢ z ∈
V |
38 | | vex 2554 |
. . . . . . 7
⊢ w ∈
V |
39 | 35, 36, 37, 38 | preq12b 3532 |
. . . . . 6
⊢
({x, y} = {z,
w} ↔ ((x = z ∧ y = w) ∨ (x = w ∧ y = z))) |
40 | 29, 34, 39 | vtoclbg 2608 |
. . . . 5
⊢ (𝐷 ∈ 𝑌 → ({x, y} =
{z, 𝐷} ↔ ((x = z ∧ y = 𝐷)
∨ (x = 𝐷 ∧ y = z)))) |
41 | 40 | a1i 9 |
. . . 4
⊢
((x ∈ 𝑉 ∧ y ∈ 𝑊 ∧ z ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({x, y} =
{z, 𝐷} ↔ ((x = z ∧ y = 𝐷)
∨ (x = 𝐷 ∧ y = z))))) |
42 | 9, 18, 27, 41 | vtocl3ga 2617 |
. . 3
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({A, B} = {𝐶, 𝐷} ↔ ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶))))) |
43 | 42 | 3expa 1103 |
. 2
⊢
(((A ∈ 𝑉 ∧ B ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({A, B} = {𝐶, 𝐷} ↔ ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶))))) |
44 | 43 | impr 361 |
1
⊢
(((A ∈ 𝑉 ∧ B ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({A, B} = {𝐶, 𝐷} ↔ ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶)))) |