Theorem breldm

Description: Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995)

	Ref	Expression
Hypotheses	opeldm.1	|- A e. _V
	opeldm.2	|- B e. _V
Assertion	breldm	|- ( A R B -> A e. dom R )

Proof

Step	Hyp	Ref	Expression
1		opeldm.1	|- A e. _V
2		opeldm.2	|- B e. _V
3		df-br	|- ( A R B <-> <. A , B >. e. R )
4	1 2	opeldm	|- ( <. A , B >. e. R -> A e. dom R )
5	3 4	sylbi	|- ( A R B -> A e. dom R )