Theorem breldmd

Description: Membership of first of a binary relation in a domain. (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	breldmd.1	|- ( ph -> A e. C )
	breldmd.2	|- ( ph -> B e. D )
	breldmd.3	|- ( ph -> A R B )
Assertion	breldmd	|- ( ph -> A e. dom R )

Proof

Step	Hyp	Ref	Expression
1		breldmd.1	|- ( ph -> A e. C )
2		breldmd.2	|- ( ph -> B e. D )
3		breldmd.3	|- ( ph -> A R B )
4		breldmg	|- ( ( A e. C /\ B e. D /\ A R B ) -> A e. dom R )
5	1 2 3 4	syl3anc	|- ( ph -> A e. dom R )