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	|- ( ( R C_ ( C X. D ) /\ A R B ) -> ( A e. C /\ B e. D ) )

Proof

Step	Hyp	Ref	Expression
1		ssbr	|- ( R C_ ( C X. D ) -> ( A R B -> A ( C X. D ) B ) )
2	1	imp	|- ( ( R C_ ( C X. D ) /\ 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	|- ( ( R C_ ( C X. D ) /\ A R B ) -> ( A e. C /\ B e. D ) )