Metamath Proof Explorer

Theorem eqopi

Description: Equality with an ordered pair. (Contributed by NM, 15-Dec-2008) (Revised by Mario Carneiro, 23-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 xpss 
 |-  ( V X. W ) C_ ( _V X. _V )
2 1 sseli 
 |-  ( A e. ( V X. W ) -> A e. ( _V X. _V ) )
3 elxp6 
 |-  ( A e. ( _V X. _V ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. _V /\ ( 2nd ` A ) e. _V ) ) )
4 3 simplbi 
 |-  ( A e. ( _V X. _V ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
5 opeq12 
 |-  ( ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) -> <. ( 1st ` A ) , ( 2nd ` A ) >. = <. B , C >. )
6 4 5 sylan9eq 
 |-  ( ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) -> A = <. B , C >. )
7 2 6 sylan 
 |-  ( ( A e. ( V X. W ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) -> A = <. B , C >. )