Metamath Proof Explorer


Theorem eqopi

Description: Equality with an ordered pair. (Contributed by NM, 15-Dec-2008) (Revised by Mario Carneiro, 23-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 xpss V × W V × V
2 1 sseli A V × W A V × V
3 elxp6 A V × V A = 1 st A 2 nd A 1 st A V 2 nd A V
4 3 simplbi A V × V A = 1 st A 2 nd A
5 opeq12 1 st A = B 2 nd A = C 1 st A 2 nd A = B C
6 4 5 sylan9eq A V × V 1 st A = B 2 nd A = C A = B C
7 2 6 sylan A V × W 1 st A = B 2 nd A = C A = B C