Theorem opeq1

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

Proof

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