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