Theorem brelg

Description: Two things in a binary relation belong to the relation's domain. (Contributed by Thierry Arnoux, 29-Aug-2017)

	Ref	Expression
Assertion	brelg	⊢ ( ( 𝑅 ⊆ ( 𝐶 × 𝐷 ) ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		ssbr	⊢ ( 𝑅 ⊆ ( 𝐶 × 𝐷 ) → ( 𝐴 𝑅 𝐵 → 𝐴 ( 𝐶 × 𝐷 ) 𝐵 ) )
2	1	imp	⊢ ( ( 𝑅 ⊆ ( 𝐶 × 𝐷 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ( 𝐶 × 𝐷 ) 𝐵 )
3		brxp	⊢ ( 𝐴 ( 𝐶 × 𝐷 ) 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )
4	2 3	sylib	⊢ ( ( 𝑅 ⊆ ( 𝐶 × 𝐷 ) ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )