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	$$⊢\phi \to A\in C$$
	breldmd.2	$$⊢\phi \to B\in D$$
	breldmd.3	$$⊢\phi \to ARB$$
Assertion	breldmd	$$⊢\phi \to A\in \mathrm{dom}R$$

Proof

Step	Hyp	Ref	Expression
1		breldmd.1	$$⊢\phi \to A\in C$$
2		breldmd.2	$$⊢\phi \to B\in D$$
3		breldmd.3	$$⊢\phi \to ARB$$
4		breldmg	$$⊢\left(A\in C\wedge B\in D\wedge ARB\right)\to A\in \mathrm{dom}R$$
5	1 2 3 4	syl3anc	$$⊢\phi \to A\in \mathrm{dom}R$$