Proof of Theorem opeqsng
Step | Hyp | Ref
| Expression |
1 | | dfopg 4803 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}) |
2 | 1 | eqeq1d 2825 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = {𝐶} ↔ {{𝐴}, {𝐴, 𝐵}} = {𝐶})) |
3 | | snex 5334 |
. . . 4
⊢ {𝐴} ∈ V |
4 | | prex 5335 |
. . . 4
⊢ {𝐴, 𝐵} ∈ V |
5 | 3, 4 | preqsn 4794 |
. . 3
⊢ ({{𝐴}, {𝐴, 𝐵}} = {𝐶} ↔ ({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶)) |
6 | 5 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({{𝐴}, {𝐴, 𝐵}} = {𝐶} ↔ ({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶))) |
7 | | eqcom 2830 |
. . . . 5
⊢ ({𝐴} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴}) |
8 | | elex 3514 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
9 | 8 | adantr 483 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ V) |
10 | | elex 3514 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
11 | 10 | adantl 484 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ V) |
12 | 9, 11 | preqsnd 4791 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} = {𝐴} ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐴))) |
13 | | simpr 487 |
. . . . . . . 8
⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐴) → 𝐵 = 𝐴) |
14 | | eqid 2823 |
. . . . . . . . 9
⊢ 𝐴 = 𝐴 |
15 | 14 | jctl 526 |
. . . . . . . 8
⊢ (𝐵 = 𝐴 → (𝐴 = 𝐴 ∧ 𝐵 = 𝐴)) |
16 | 13, 15 | impbii 211 |
. . . . . . 7
⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐴) ↔ 𝐵 = 𝐴) |
17 | | eqcom 2830 |
. . . . . . 7
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
18 | 16, 17 | bitri 277 |
. . . . . 6
⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐴) ↔ 𝐴 = 𝐵) |
19 | 12, 18 | syl6bb 289 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐵} = {𝐴} ↔ 𝐴 = 𝐵)) |
20 | 7, 19 | syl5bb 285 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} = {𝐴, 𝐵} ↔ 𝐴 = 𝐵)) |
21 | 20 | anbi1d 631 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶))) |
22 | | dfsn2 4582 |
. . . . . . . 8
⊢ {𝐴} = {𝐴, 𝐴} |
23 | | preq2 4672 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
24 | 22, 23 | syl5req 2871 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴}) |
25 | 24 | eqeq1d 2825 |
. . . . . 6
⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ {𝐴} = 𝐶)) |
26 | | eqcom 2830 |
. . . . . 6
⊢ ({𝐴} = 𝐶 ↔ 𝐶 = {𝐴}) |
27 | 25, 26 | syl6bb 289 |
. . . . 5
⊢ (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ 𝐶 = {𝐴})) |
28 | 27 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 = 𝐵 → ({𝐴, 𝐵} = 𝐶 ↔ 𝐶 = {𝐴}))) |
29 | 28 | pm5.32d 579 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 = 𝐵 ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴}))) |
30 | 21, 29 | bitrd 281 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (({𝐴} = {𝐴, 𝐵} ∧ {𝐴, 𝐵} = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴}))) |
31 | 2, 6, 30 | 3bitrd 307 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴}))) |