Metamath Proof Explorer

Theorem opelxp1

Description: The first member of an ordered pair of classes in a Cartesian product belongs to first Cartesian product argument. (Contributed by NM, 28-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opelxp1 A B C × D A C


Step Hyp Ref Expression
1 opelxp A B C × D A C B D
2 1 simplbi A B C × D A C