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 )