Step | Hyp | Ref
| Expression |
1 | | eleq1 2877 |
. . . 4
⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) |
2 | | preq2 4630 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
3 | 2 | preq2d 4636 |
. . . . 5
⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}}) |
4 | 3 | eleq2d 2875 |
. . . 4
⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})) |
5 | 1, 4 | 3anbi23d 1436 |
. . 3
⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))) |
6 | 5 | abbidv 2862 |
. 2
⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}) |
7 | | df-op 4532 |
. 2
⊢
〈𝐶, 𝐴〉 = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} |
8 | | df-op 4532 |
. 2
⊢
〈𝐶, 𝐵〉 = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})} |
9 | 6, 7, 8 | 3eqtr4g 2858 |
1
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |