Metamath Proof Explorer

Theorem relelrn

Description: The second argument of a binary relation belongs to its range. (Contributed by NM, 2-Jul-2008)

		Ref	Expression
	Assertion	relelrn	$⊢ (Rel R \land A R B) \to B \in ran R$

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		brelrng	$⊢ (A \in V \land B \in V \land A R B) \to B \in ran R$
5	1 2 3 4	syl3anc	$⊢ (Rel R \land A R B) \to B \in ran R$