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