Proof of Theorem opeqsn
Step | Hyp | Ref
| Expression |
1 | | opeqsn.1 |
. . . 4
⊢ A ∈
V |
2 | | opeqsn.2 |
. . . 4
⊢ B ∈
V |
3 | 1, 2 | dfop 3539 |
. . 3
⊢
〈A, B〉 = {{A},
{A, B}} |
4 | 3 | eqeq1i 2044 |
. 2
⊢
(〈A, B〉 = {𝐶} ↔ {{A}, {A, B}} = {𝐶}) |
5 | | snexgOLD 3926 |
. . . 4
⊢ (A ∈ V →
{A} ∈
V) |
6 | 1, 5 | ax-mp 7 |
. . 3
⊢ {A} ∈
V |
7 | | prexgOLD 3937 |
. . . 4
⊢
((A ∈ V ∧ B ∈ V) →
{A, B}
∈ V) |
8 | 1, 2, 7 | mp2an 402 |
. . 3
⊢ {A, B} ∈ V |
9 | | opeqsn.3 |
. . 3
⊢ 𝐶 ∈ V |
10 | 6, 8, 9 | preqsn 3537 |
. 2
⊢
({{A}, {A, B}} = {𝐶} ↔ ({A} = {A,
B} ∧
{A, B}
= 𝐶)) |
11 | | eqcom 2039 |
. . . . 5
⊢
({A} = {A, B} ↔
{A, B}
= {A}) |
12 | 1, 2, 1 | preqsn 3537 |
. . . . 5
⊢
({A, B} = {A} ↔
(A = B
∧ B =
A)) |
13 | | eqcom 2039 |
. . . . . . 7
⊢ (B = A ↔
A = B) |
14 | 13 | anbi2i 430 |
. . . . . 6
⊢
((A = B ∧ B = A) ↔
(A = B
∧ A =
B)) |
15 | | anidm 376 |
. . . . . 6
⊢
((A = B ∧ A = B) ↔
A = B) |
16 | 14, 15 | bitri 173 |
. . . . 5
⊢
((A = B ∧ B = A) ↔
A = B) |
17 | 11, 12, 16 | 3bitri 195 |
. . . 4
⊢
({A} = {A, B} ↔
A = B) |
18 | 17 | anbi1i 431 |
. . 3
⊢
(({A} = {A, B} ∧ {A, B} = 𝐶) ↔ (A = B ∧ {A, B} = 𝐶)) |
19 | | dfsn2 3381 |
. . . . . . 7
⊢ {A} = {A,
A} |
20 | | preq2 3439 |
. . . . . . 7
⊢ (A = B →
{A, A}
= {A, B}) |
21 | 19, 20 | syl5req 2082 |
. . . . . 6
⊢ (A = B →
{A, B}
= {A}) |
22 | 21 | eqeq1d 2045 |
. . . . 5
⊢ (A = B →
({A, B}
= 𝐶 ↔ {A} = 𝐶)) |
23 | | eqcom 2039 |
. . . . 5
⊢
({A} = 𝐶 ↔ 𝐶 = {A}) |
24 | 22, 23 | syl6bb 185 |
. . . 4
⊢ (A = B →
({A, B}
= 𝐶 ↔ 𝐶 = {A})) |
25 | 24 | pm5.32i 427 |
. . 3
⊢
((A = B ∧ {A, B} = 𝐶) ↔ (A = B ∧ 𝐶 = {A})) |
26 | 18, 25 | bitri 173 |
. 2
⊢
(({A} = {A, B} ∧ {A, B} = 𝐶) ↔ (A = B ∧ 𝐶 = {A})) |
27 | 4, 10, 26 | 3bitri 195 |
1
⊢
(〈A, B〉 = {𝐶} ↔ (A = B ∧ 𝐶 = {A})) |