Proof of Theorem opeqsn
Step | Hyp | Ref
| Expression |
1 | | opeqsn.1 |
. . . 4
⊢ 𝐴 ∈ V |
2 | | opeqsn.2 |
. . . 4
⊢ 𝐵 ∈ V |
3 | 1, 2 | dfop 3548 |
. . 3
⊢
〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}} |
4 | 3 | eqeq1i 2047 |
. 2
⊢
(〈𝐴, 𝐵〉 = {𝐶} ↔ {{𝐴}, {𝐴, 𝐵}} = {𝐶}) |
5 | | snexgOLD 3935 |
. . . 4
⊢ (𝐴 ∈ V → {𝐴} ∈ V) |
6 | 1, 5 | ax-mp 7 |
. . 3
⊢ {𝐴} ∈ V |
7 | | prexgOLD 3946 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V) |
8 | 1, 2, 7 | mp2an 402 |
. . 3
⊢ {𝐴, 𝐵} ∈ V |
9 | | opeqsn.3 |
. . 3
⊢ 𝐶 ∈ V |
10 | 6, 8, 9 | preqsn 3546 |
. 2
⊢ ({{𝐴}, {𝐴, 𝐵}} = {𝐶} ↔ ({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶)) |
11 | | eqcom 2042 |
. . . . 5
⊢ ({𝐴} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴}) |
12 | 1, 2, 1 | preqsn 3546 |
. . . . 5
⊢ ({𝐴, 𝐵} = {𝐴} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐴)) |
13 | | eqcom 2042 |
. . . . . . 7
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
14 | 13 | anbi2i 430 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐴 = 𝐵)) |
15 | | anidm 376 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐵) ↔ 𝐴 = 𝐵) |
16 | 14, 15 | bitri 173 |
. . . . 5
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐴) ↔ 𝐴 = 𝐵) |
17 | 11, 12, 16 | 3bitri 195 |
. . . 4
⊢ ({𝐴} = {𝐴, 𝐵} ↔ 𝐴 = 𝐵) |
18 | 17 | anbi1i 431 |
. . 3
⊢ (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶)) |
19 | | dfsn2 3389 |
. . . . . . 7
⊢ {𝐴} = {𝐴, 𝐴} |
20 | | preq2 3448 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
21 | 19, 20 | syl5req 2085 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴}) |
22 | 21 | eqeq1d 2048 |
. . . . 5
⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ {𝐴} = 𝐶)) |
23 | | eqcom 2042 |
. . . . 5
⊢ ({𝐴} = 𝐶 ↔ 𝐶 = {𝐴}) |
24 | 22, 23 | syl6bb 185 |
. . . 4
⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ 𝐶 = {𝐴})) |
25 | 24 | pm5.32i 427 |
. . 3
⊢ ((𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) |
26 | 18, 25 | bitri 173 |
. 2
⊢ (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) |
27 | 4, 10, 26 | 3bitri 195 |
1
⊢
(〈𝐴, 𝐵〉 = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) |