Proof of Theorem opeq1
| Step | Hyp | Ref
| Expression |
| 1 | | eleq1 2829 |
. . . 4
⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) |
| 2 | 1 | anbi1d 631 |
. . 3
⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V))) |
| 3 | | sneq 4636 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) |
| 4 | | preq1 4733 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
| 5 | 3, 4 | preq12d 4741 |
. . 3
⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}}) |
| 6 | 2, 5 | ifbieq1d 4550 |
. 2
⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)) |
| 7 | | dfopif 4870 |
. 2
⊢
〈𝐴, 𝐶〉 = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) |
| 8 | | dfopif 4870 |
. 2
⊢
〈𝐵, 𝐶〉 = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅) |
| 9 | 6, 7, 8 | 3eqtr4g 2802 |
1
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |