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