Metamath Proof Explorer


Theorem brel

Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypothesis brel.1
|- R C_ ( C X. D )
Assertion brel
|- ( A R B -> ( A e. C /\ B e. D ) )

Proof

Step Hyp Ref Expression
1 brel.1
 |-  R C_ ( C X. D )
2 1 ssbri
 |-  ( A R B -> A ( C X. D ) B )
3 brxp
 |-  ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
4 2 3 sylib
 |-  ( A R B -> ( A e. C /\ B e. D ) )