Theorem 1st2nd2

Description: Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013)

	Ref	Expression
Assertion	1st2nd2	|- ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )

Proof

Step	Hyp	Ref	Expression
1		elxp6	|- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
2	1	simplbi	|- ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )