Metamath Proof Explorer


Theorem opelxp

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opelxp ABC×DACBD

Proof

Step Hyp Ref Expression
1 elxp2 ABC×DxCyDAB=xy
2 vex xV
3 vex yV
4 2 3 opth2 AB=xyA=xB=y
5 eleq1 A=xACxC
6 eleq1 B=yBDyD
7 5 6 bi2anan9 A=xB=yACBDxCyD
8 4 7 sylbi AB=xyACBDxCyD
9 8 biimprcd xCyDAB=xyACBD
10 9 rexlimivv xCyDAB=xyACBD
11 eqid AB=AB
12 opeq1 x=Axy=Ay
13 12 eqeq2d x=AAB=xyAB=Ay
14 opeq2 y=BAy=AB
15 14 eqeq2d y=BAB=AyAB=AB
16 13 15 rspc2ev ACBDAB=ABxCyDAB=xy
17 11 16 mp3an3 ACBDxCyDAB=xy
18 10 17 impbii xCyDAB=xyACBD
19 1 18 bitri ABC×DACBD