Theorem 2ndrn

Description: The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	2ndrn	|- ( ( Rel R /\ A e. R ) -> ( 2nd ` A ) e. ran R )

Proof

Step	Hyp	Ref	Expression
1		1st2nd	|- ( ( Rel R /\ A e. R ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
2		simpr	|- ( ( Rel R /\ A e. R ) -> A e. R )
3	1 2	eqeltrrd	|- ( ( Rel R /\ A e. R ) -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. R )
4		fvex	|- ( 1st ` A ) e. _V
5		fvex	|- ( 2nd ` A ) e. _V
6	4 5	opelrn	|- ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. R -> ( 2nd ` A ) e. ran R )
7	3 6	syl	|- ( ( Rel R /\ A e. R ) -> ( 2nd ` A ) e. ran R )