Description: Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007) (Proof shortened by Mario Carneiro, 26-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eqop | |- ( A e. ( V X. W ) -> ( A = <. B , C >. <-> ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1st2nd2 | |- ( A e. ( V X. W ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. ) |
|
| 2 | 1 | eqeq1d | |- ( A e. ( V X. W ) -> ( A = <. B , C >. <-> <. ( 1st ` A ) , ( 2nd ` A ) >. = <. B , C >. ) ) |
| 3 | fvex | |- ( 1st ` A ) e. _V |
|
| 4 | fvex | |- ( 2nd ` A ) e. _V |
|
| 5 | 3 4 | opth | |- ( <. ( 1st ` A ) , ( 2nd ` A ) >. = <. B , C >. <-> ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) |
| 6 | 2 5 | bitrdi | |- ( A e. ( V X. W ) -> ( A = <. B , C >. <-> ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) ) |