Theorem 1st2ndb

Description: Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	|- ( A e. ( _V X. _V ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
2		id	|- ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
3		fvex	|- ( 1st ` A ) e. _V
4		fvex	|- ( 2nd ` A ) e. _V
5	3 4	opelvv	|- <. ( 1st ` A ) , ( 2nd ` A ) >. e. ( _V X. _V )
6	2 5	eqeltrdi	|- ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. -> A e. ( _V X. _V ) )
7	1 6	impbii	|- ( A e. ( _V X. _V ) <-> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )