Metamath Proof Explorer


Theorem eqop

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007) (Proof shortened by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion eqop A V × W A = B C 1 st A = B 2 nd A = C

Proof

Step Hyp Ref Expression
1 1st2nd2 A V × W A = 1 st A 2 nd A
2 1 eqeq1d A V × W A = B C 1 st A 2 nd A = B C
3 fvex 1 st A V
4 fvex 2 nd A V
5 3 4 opth 1 st A 2 nd A = B C 1 st A = B 2 nd A = C
6 2 5 bitrdi A V × W A = B C 1 st A = B 2 nd A = C