Proof of Theorem opeqsn
Step | Hyp | Ref
| Expression |
1 | | opeqsn.1 |
. . . 4
⊢ 𝐴 ∈ V |
2 | | opeqsn.2 |
. . . 4
⊢ 𝐵 ∈ V |
3 | 1, 2 | dfop 4339 |
. . 3
⊢
〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}} |
4 | 3 | eqeq1i 2615 |
. 2
⊢
(〈𝐴, 𝐵〉 = {𝐶} ↔ {{𝐴}, {𝐴, 𝐵}} = {𝐶}) |
5 | | snex 4835 |
. . 3
⊢ {𝐴} ∈ V |
6 | | prex 4836 |
. . 3
⊢ {𝐴, 𝐵} ∈ V |
7 | | opeqsn.3 |
. . 3
⊢ 𝐶 ∈ V |
8 | 5, 6, 7 | preqsn 4331 |
. 2
⊢ ({{𝐴}, {𝐴, 𝐵}} = {𝐶} ↔ ({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶)) |
9 | | eqcom 2617 |
. . . . 5
⊢ ({𝐴} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴}) |
10 | 1, 2, 1 | preqsn 4331 |
. . . . 5
⊢ ({𝐴, 𝐵} = {𝐴} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐴)) |
11 | | eqcom 2617 |
. . . . . . 7
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
12 | 11 | anbi2i 726 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐴 = 𝐵)) |
13 | | anidm 674 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐵) ↔ 𝐴 = 𝐵) |
14 | 12, 13 | bitri 263 |
. . . . 5
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐴) ↔ 𝐴 = 𝐵) |
15 | 9, 10, 14 | 3bitri 285 |
. . . 4
⊢ ({𝐴} = {𝐴, 𝐵} ↔ 𝐴 = 𝐵) |
16 | 15 | anbi1i 727 |
. . 3
⊢ (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶)) |
17 | | dfsn2 4138 |
. . . . . . 7
⊢ {𝐴} = {𝐴, 𝐴} |
18 | | preq2 4213 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
19 | 17, 18 | syl5req 2657 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴}) |
20 | 19 | eqeq1d 2612 |
. . . . 5
⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ {𝐴} = 𝐶)) |
21 | | eqcom 2617 |
. . . . 5
⊢ ({𝐴} = 𝐶 ↔ 𝐶 = {𝐴}) |
22 | 20, 21 | syl6bb 275 |
. . . 4
⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ 𝐶 = {𝐴})) |
23 | 22 | pm5.32i 667 |
. . 3
⊢ ((𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) |
24 | 16, 23 | bitri 263 |
. 2
⊢ (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) |
25 | 4, 8, 24 | 3bitri 285 |
1
⊢
(〈𝐴, 𝐵〉 = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) |