This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opeq1

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ↔ 𝐵 ∈ V ) )
2 1 anbi1d ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ↔ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) )
3 sneq ⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐵 } )
4 preq1 ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } )
5 3 4 preq12d ⊢ ( 𝐴 = 𝐵 → { { 𝐴 } , { 𝐴 , 𝐶 } } = { { 𝐵 } , { 𝐵 , 𝐶 } } )
6 2 5 ifbieq1d ⊢ ( 𝐴 = 𝐵 → if ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐶 } } , ∅ ) = if ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) , { { 𝐵 } , { 𝐵 , 𝐶 } } , ∅ ) )
7 dfopif ⊢ ⟨ 𝐴 , 𝐶 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐶 } } , ∅ )
8 dfopif ⊢ ⟨ 𝐵 , 𝐶 ⟩ = if ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) , { { 𝐵 } , { 𝐵 , 𝐶 } } , ∅ )
9 6 7 8 3eqtr4g ⊢ ( 𝐴 = 𝐵 → ⟨ 𝐴 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )