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 RC×D
Assertion brel ARBACBD

Proof

Step Hyp Ref Expression
1 brel.1 RC×D
2 1 ssbri ARBAC×DB
3 brxp AC×DBACBD
4 2 3 sylib ARBACBD