# Metamath Proof Explorer

## Theorem opeq1

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

### Proof

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