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