Theorem releldmi

Description: The first argument of a binary relation belongs to its domain. (Contributed by NM, 28-Apr-2015)

	Ref	Expression
Hypothesis	releldm.1	$$⊢\mathrm{Rel}R$$
Assertion	releldmi	$$⊢ARB\to A\in \mathrm{dom}R$$

Proof

Step	Hyp	Ref	Expression
1		releldm.1	$$⊢\mathrm{Rel}R$$
2		releldm	$$⊢\left(\mathrm{Rel}R\wedge ARB\right)\to A\in \mathrm{dom}R$$
3	1 2	mpan	$$⊢ARB\to A\in \mathrm{dom}R$$