Theorem eqop2

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014)

	Ref	Expression
Hypotheses	eqop2.1	|- B e. _V
	eqop2.2	|- C e. _V
Assertion	eqop2	|- ( A = <. B , C >. <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqop2.1	|- B e. _V
2		eqop2.2	|- C e. _V
3	1 2	opelvv	|- <. B , C >. e. ( _V X. _V )
4		eleq1	|- ( A = <. B , C >. -> ( A e. ( _V X. _V ) <-> <. B , C >. e. ( _V X. _V ) ) )
5	3 4	mpbiri	|- ( A = <. B , C >. -> A e. ( _V X. _V ) )
6		eqop	|- ( A e. ( _V X. _V ) -> ( A = <. B , C >. <-> ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) )
7	5 6	biadanii	|- ( A = <. B , C >. <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) )