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 e. dom R )

Proof

Step Hyp Ref Expression
1 releldm.1 
 |-  Rel R
2 releldm 
 |-  ( ( Rel R /\ A R B ) -> A e. dom R )
3 1 2 mpan 
 |-  ( A R B -> A e. dom R )