Theorem opeq2

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

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ↔ 𝐵 ∈ V ) )
2		preq2	⊢ ( 𝐴 = 𝐵 → { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } )
3	2	preq2d	⊢ ( 𝐴 = 𝐵 → { { 𝐶 } , { 𝐶 , 𝐴 } } = { { 𝐶 } , { 𝐶 , 𝐵 } } )
4	3	eleq2d	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐴 } } ↔ 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐵 } } ) )
5	1 4	3anbi23d	⊢ ( 𝐴 = 𝐵 → ( ( 𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐴 } } ) ↔ ( 𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐵 } } ) ) )
6	5	abbidv	⊢ ( 𝐴 = 𝐵 → { 𝑥 ∣ ( 𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐴 } } ) } = { 𝑥 ∣ ( 𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐵 } } ) } )
7		df-op	⊢ ⟨ 𝐶 , 𝐴 ⟩ = { 𝑥 ∣ ( 𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐴 } } ) }
8		df-op	⊢ ⟨ 𝐶 , 𝐵 ⟩ = { 𝑥 ∣ ( 𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐶 } , { 𝐶 , 𝐵 } } ) }
9	6 7 8	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ )