This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \land A R B) \to A \in dom R$

Proof

Step	Hyp	Ref	Expression
1		brrelex1	$⊢ (Rel R \land A R B) \to A \in V$
2		brrelex2	$⊢ (Rel R \land A R B) \to B \in V$
3		simpr	$⊢ (Rel R \land A R B) \to A R B$
4		breldmg	$⊢ (A \in V \land B \in V \land A R B) \to A \in dom R$
5	1 2 3 4	syl3anc	$⊢ (Rel R \land A R B) \to A \in dom R$