This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opth1

Description: Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses opth1.1 
|- A e. _V
opth1.2 
|- B e. _V
Assertion opth1 
|- ( <. A , B >. = <. C , D >. -> A = C )

Proof

Step Hyp Ref Expression
1 opth1.1 
 |-  A e. _V
2 opth1.2 
 |-  B e. _V
3 1 2 opi1 
 |-  { A } e. <. A , B >.
4 id 
 |-  ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
5 3 4 eleqtrid 
 |-  ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
6 1 sneqr 
 |-  ( { A } = { C } -> A = C )
7 6 a1i 
 |-  ( { A } e. <. C , D >. -> ( { A } = { C } -> A = C ) )
8 oprcl 
 |-  ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )
9 8 simpld 
 |-  ( { A } e. <. C , D >. -> C e. _V )
10 prid1g 
 |-  ( C e. _V -> C e. { C , D } )
11 9 10 syl 
 |-  ( { A } e. <. C , D >. -> C e. { C , D } )
12 eleq2 
 |-  ( { A } = { C , D } -> ( C e. { A } <-> C e. { C , D } ) )
13 11 12 syl5ibrcom 
 |-  ( { A } e. <. C , D >. -> ( { A } = { C , D } -> C e. { A } ) )
14 elsni 
 |-  ( C e. { A } -> C = A )
15 14 eqcomd 
 |-  ( C e. { A } -> A = C )
16 13 15 syl6 
 |-  ( { A } e. <. C , D >. -> ( { A } = { C , D } -> A = C ) )
17 id 
 |-  ( { A } e. <. C , D >. -> { A } e. <. C , D >. )
18 dfopg 
 |-  ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )
19 8 18 syl 
 |-  ( { A } e. <. C , D >. -> <. C , D >. = { { C } , { C , D } } )
20 17 19 eleqtrd 
 |-  ( { A } e. <. C , D >. -> { A } e. { { C } , { C , D } } )
21 elpri 
 |-  ( { A } e. { { C } , { C , D } } -> ( { A } = { C } \/ { A } = { C , D } ) )
22 20 21 syl 
 |-  ( { A } e. <. C , D >. -> ( { A } = { C } \/ { A } = { C , D } ) )
23 7 16 22 mpjaod 
 |-  ( { A } e. <. C , D >. -> A = C )
24 5 23 syl 
 |-  ( <. A , B >. = <. C , D >. -> A = C )