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=BAC=BC

Proof

Step Hyp Ref Expression
1 eleq1 A=BAVBV
2 1 anbi1d A=BAVCVBVCV
3 sneq A=BA=B
4 preq1 A=BAC=BC
5 3 4 preq12d A=BAAC=BBC
6 2 5 ifbieq1d A=BifAVCVAAC=ifBVCVBBC
7 dfopif AC=ifAVCVAAC
8 dfopif BC=ifBVCVBBC
9 6 7 8 3eqtr4g A=BAC=BC