Step | Hyp | Ref
| Expression |
1 | | preq1 3799 |
. . . . . . 7
⊢ (x = A →
{x, y}
= {A, y}) |
2 | 1 | eqeq1d 2361 |
. . . . . 6
⊢ (x = A →
({x, y}
= {z, D} ↔ {A,
y} = {z, D})) |
3 | | eqeq1 2359 |
. . . . . . . 8
⊢ (x = A →
(x = z
↔ A = z)) |
4 | 3 | anbi1d 685 |
. . . . . . 7
⊢ (x = A →
((x = z
∧ y =
D) ↔ (A = z ∧ y = D))) |
5 | | eqeq1 2359 |
. . . . . . . 8
⊢ (x = A →
(x = D
↔ A = D)) |
6 | 5 | anbi1d 685 |
. . . . . . 7
⊢ (x = A →
((x = D
∧ y =
z) ↔ (A = D ∧ y = z))) |
7 | 4, 6 | orbi12d 690 |
. . . . . 6
⊢ (x = A →
(((x = z ∧ y = D) ∨ (x = D ∧ y = z)) ↔
((A = z
∧ y =
D) ∨
(A = D
∧ y =
z)))) |
8 | 2, 7 | bibi12d 312 |
. . . . 5
⊢ (x = A →
(({x, y} = {z,
D} ↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z))) ↔ ({A,
y} = {z, D} ↔
((A = z
∧ y =
D) ∨
(A = D
∧ y =
z))))) |
9 | 8 | imbi2d 307 |
. . . 4
⊢ (x = A →
((D ∈
Y → ({x, y} =
{z, D}
↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z)))) ↔
(D ∈
Y → ({A, y} =
{z, D}
↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z)))))) |
10 | | preq2 3800 |
. . . . . . 7
⊢ (y = B →
{A, y}
= {A, B}) |
11 | 10 | eqeq1d 2361 |
. . . . . 6
⊢ (y = B →
({A, y}
= {z, D} ↔ {A,
B} = {z, D})) |
12 | | eqeq1 2359 |
. . . . . . . 8
⊢ (y = B →
(y = D
↔ B = D)) |
13 | 12 | anbi2d 684 |
. . . . . . 7
⊢ (y = B →
((A = z
∧ y =
D) ↔ (A = z ∧ B = D))) |
14 | | eqeq1 2359 |
. . . . . . . 8
⊢ (y = B →
(y = z
↔ B = z)) |
15 | 14 | anbi2d 684 |
. . . . . . 7
⊢ (y = B →
((A = D
∧ y =
z) ↔ (A = D ∧ B = z))) |
16 | 13, 15 | orbi12d 690 |
. . . . . 6
⊢ (y = B →
(((A = z ∧ y = D) ∨ (A = D ∧ y = z)) ↔
((A = z
∧ B =
D) ∨
(A = D
∧ B =
z)))) |
17 | 11, 16 | bibi12d 312 |
. . . . 5
⊢ (y = B →
(({A, y} = {z,
D} ↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z))) ↔ ({A,
B} = {z, D} ↔
((A = z
∧ B =
D) ∨
(A = D
∧ B =
z))))) |
18 | 17 | imbi2d 307 |
. . . 4
⊢ (y = B →
((D ∈
Y → ({A, y} =
{z, D}
↔ ((A = z ∧ y = D) ∨ (A = D ∧ y = z)))) ↔
(D ∈
Y → ({A, B} =
{z, D}
↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z)))))) |
19 | | preq1 3799 |
. . . . . . 7
⊢ (z = C →
{z, D}
= {C, D}) |
20 | 19 | eqeq2d 2364 |
. . . . . 6
⊢ (z = C →
({A, B}
= {z, D} ↔ {A,
B} = {C, D})) |
21 | | eqeq2 2362 |
. . . . . . . 8
⊢ (z = C →
(A = z
↔ A = C)) |
22 | 21 | anbi1d 685 |
. . . . . . 7
⊢ (z = C →
((A = z
∧ B =
D) ↔ (A = C ∧ B = D))) |
23 | | eqeq2 2362 |
. . . . . . . 8
⊢ (z = C →
(B = z
↔ B = C)) |
24 | 23 | anbi2d 684 |
. . . . . . 7
⊢ (z = C →
((A = D
∧ B =
z) ↔ (A = D ∧ B = C))) |
25 | 22, 24 | orbi12d 690 |
. . . . . 6
⊢ (z = C →
(((A = z ∧ B = D) ∨ (A = D ∧ B = z)) ↔
((A = C
∧ B =
D) ∨
(A = D
∧ B =
C)))) |
26 | 20, 25 | bibi12d 312 |
. . . . 5
⊢ (z = C →
(({A, B} = {z,
D} ↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z))) ↔ ({A,
B} = {C, D} ↔
((A = C
∧ B =
D) ∨
(A = D
∧ B =
C))))) |
27 | 26 | imbi2d 307 |
. . . 4
⊢ (z = C →
((D ∈
Y → ({A, B} =
{z, D}
↔ ((A = z ∧ B = D) ∨ (A = D ∧ B = z)))) ↔
(D ∈
Y → ({A, B} =
{C, D}
↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C)))))) |
28 | | preq2 3800 |
. . . . . . 7
⊢ (w = D →
{z, w}
= {z, D}) |
29 | 28 | eqeq2d 2364 |
. . . . . 6
⊢ (w = D →
({x, y}
= {z, w} ↔ {x,
y} = {z, D})) |
30 | | eqeq2 2362 |
. . . . . . . 8
⊢ (w = D →
(y = w
↔ y = D)) |
31 | 30 | anbi2d 684 |
. . . . . . 7
⊢ (w = D →
((x = z
∧ y =
w) ↔ (x = z ∧ y = D))) |
32 | | eqeq2 2362 |
. . . . . . . 8
⊢ (w = D →
(x = w
↔ x = D)) |
33 | 32 | anbi1d 685 |
. . . . . . 7
⊢ (w = D →
((x = w
∧ y =
z) ↔ (x = D ∧ y = z))) |
34 | 31, 33 | orbi12d 690 |
. . . . . 6
⊢ (w = D →
(((x = z ∧ y = w) ∨ (x = w ∧ y = z)) ↔
((x = z
∧ y =
D) ∨
(x = D
∧ y =
z)))) |
35 | | vex 2862 |
. . . . . . 7
⊢ x ∈
V |
36 | | vex 2862 |
. . . . . . 7
⊢ y ∈
V |
37 | | vex 2862 |
. . . . . . 7
⊢ z ∈
V |
38 | | vex 2862 |
. . . . . . 7
⊢ w ∈
V |
39 | 35, 36, 37, 38 | preq12b 4127 |
. . . . . 6
⊢ ({x, y} =
{z, w}
↔ ((x = z ∧ y = w) ∨ (x = w ∧ y = z))) |
40 | 29, 34, 39 | vtoclbg 2915 |
. . . . 5
⊢ (D ∈ Y → ({x,
y} = {z, D} ↔
((x = z
∧ y =
D) ∨
(x = D
∧ y =
z)))) |
41 | 40 | a1i 10 |
. . . 4
⊢ ((x ∈ V ∧ y ∈ W ∧ z ∈ X) → (D
∈ Y
→ ({x, y} = {z,
D} ↔ ((x = z ∧ y = D) ∨ (x = D ∧ y = z))))) |
42 | 9, 18, 27, 41 | vtocl3ga 2924 |
. . 3
⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (D
∈ Y
→ ({A, B} = {C,
D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C))))) |
43 | 42 | 3expa 1151 |
. 2
⊢ (((A ∈ V ∧ B ∈ W) ∧ C ∈ X) → (D
∈ Y
→ ({A, B} = {C,
D} ↔ ((A = C ∧ B = D) ∨ (A = D ∧ B = C))))) |
44 | 43 | impr 602 |
1
⊢ (((A ∈ V ∧ B ∈ W) ∧ (C ∈ X ∧ D ∈ Y)) → ({A,
B} = {C, D} ↔
((A = C
∧ B =
D) ∨
(A = D
∧ B =
C)))) |