Theorem 1st2nd

Description: Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006)

	Ref	Expression
Assertion	1st2nd	|- ( ( Rel B /\ A e. B ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )

Proof

Step	Hyp	Ref	Expression
1		df-rel	|- ( Rel B <-> B C_ ( _V X. _V ) )
2		ssel2	|- ( ( B C_ ( _V X. _V ) /\ A e. B ) -> A e. ( _V X. _V ) )
3	1 2	sylanb	|- ( ( Rel B /\ A e. B ) -> A e. ( _V X. _V ) )
4		1st2nd2	|- ( A e. ( _V X. _V ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
5	3 4	syl	|- ( ( Rel B /\ A e. B ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )