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 𝑅 ⊆ ( 𝐶 × 𝐷 )
Assertion brel ( 𝐴 𝑅 𝐵 → ( 𝐴𝐶𝐵𝐷 ) )

Proof

Step Hyp Ref Expression
1 brel.1 𝑅 ⊆ ( 𝐶 × 𝐷 )
2 1 ssbri ( 𝐴 𝑅 𝐵𝐴 ( 𝐶 × 𝐷 ) 𝐵 )
3 brxp ( 𝐴 ( 𝐶 × 𝐷 ) 𝐵 ↔ ( 𝐴𝐶𝐵𝐷 ) )
4 2 3 sylib ( 𝐴 𝑅 𝐵 → ( 𝐴𝐶𝐵𝐷 ) )