# Metamath Proof Explorer

## Theorem opeq2

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 26-May-2024)

Ref Expression
Assertion opeq2 ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ )

### Proof

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 ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ )