# Metamath Proof Explorer

## 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 ${⊢}{A}={B}\to ⟨{A},{C}⟩=⟨{B},{C}⟩$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{A}={B}\to \left({A}\in \mathrm{V}↔{B}\in \mathrm{V}\right)$
2 1 anbi1d ${⊢}{A}={B}\to \left(\left({A}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)↔\left({B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\right)$
3 sneq ${⊢}{A}={B}\to \left\{{A}\right\}=\left\{{B}\right\}$
4 preq1 ${⊢}{A}={B}\to \left\{{A},{C}\right\}=\left\{{B},{C}\right\}$
5 3 4 preq12d ${⊢}{A}={B}\to \left\{\left\{{A}\right\},\left\{{A},{C}\right\}\right\}=\left\{\left\{{B}\right\},\left\{{B},{C}\right\}\right\}$
6 2 5 ifbieq1d ${⊢}{A}={B}\to if\left(\left({A}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right),\left\{\left\{{A}\right\},\left\{{A},{C}\right\}\right\},\varnothing \right)=if\left(\left({B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right),\left\{\left\{{B}\right\},\left\{{B},{C}\right\}\right\},\varnothing \right)$
7 dfopif ${⊢}⟨{A},{C}⟩=if\left(\left({A}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right),\left\{\left\{{A}\right\},\left\{{A},{C}\right\}\right\},\varnothing \right)$
8 dfopif ${⊢}⟨{B},{C}⟩=if\left(\left({B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right),\left\{\left\{{B}\right\},\left\{{B},{C}\right\}\right\},\varnothing \right)$
9 6 7 8 3eqtr4g ${⊢}{A}={B}\to ⟨{A},{C}⟩=⟨{B},{C}⟩$