Metamath Proof Explorer

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 Rel R
Assertion releldmi A R B A dom R


Step Hyp Ref Expression
1 releldm.1 Rel R
2 releldm Rel R A R B A dom R
3 1 2 mpan A R B A dom R