Theorem releldm

Description: The first argument of a binary relation belongs to its domain. Note that A R B does not imply Rel R : see for example nrelv and brv . (Contributed by NM, 2-Jul-2008)

	Ref	Expression
Assertion	releldm	|- ( ( Rel R /\ A R B ) -> A e. dom R )

Proof

Step	Hyp	Ref	Expression
1		brrelex1	|- ( ( Rel R /\ A R B ) -> A e. _V )
2		brrelex2	|- ( ( Rel R /\ A R B ) -> B e. _V )
3		simpr	|- ( ( Rel R /\ A R B ) -> A R B )
4		breldmg	|- ( ( A e. _V /\ B e. _V /\ A R B ) -> A e. dom R )
5	1 2 3 4	syl3anc	|- ( ( Rel R /\ A R B ) -> A e. dom R )