Theorem opelrn

Description: Membership of second member of an ordered pair in a range. (Contributed by NM, 23-Feb-1997)

	Ref	Expression
Hypotheses	brelrn.1	|- A e. _V
	brelrn.2	|- B e. _V
Assertion	opelrn	|- ( <. A , B >. e. C -> B e. ran C )

Proof

Step	Hyp	Ref	Expression
1		brelrn.1	|- A e. _V
2		brelrn.2	|- B e. _V
3		df-br	|- ( A C B <-> <. A , B >. e. C )
4	1 2	brelrn	|- ( A C B -> B e. ran C )
5	3 4	sylbir	|- ( <. A , B >. e. C -> B e. ran C )