Metamath Proof Explorer

Theorem brxp

Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004)

Ref Expression
Assertion brxp 
|- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( A ( C X. D ) B <-> <. A , B >. e. ( C X. D ) )
2 opelxp 
 |-  ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
3 1 2 bitri 
 |-  ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )