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	⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )