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

Metamath Proof Explorer

Theorem opeq2

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

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

Proof

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