Theorem opth1 4675

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

Hypotheses

Ref	Expression
opth1.1	|- A e. _V
opth1.2	|- B e. _V

Assertion

Ref	Expression
opth1	|- ( <. A , B >. = <. C , D >. -> A = C )

Proof of Theorem opth1

Step	Hyp	Ref	Expression
1		opth1.1	. . . 4 |- A e. _V
2	1	sneqr 4139	. . 3 |- ( { A } = { C } -> A = C )
3	2	a1i 11	. 2 |- ( <. A , B >. = <. C , D >. -> ( { A } = { C } -> A = C ) )
4		opth1.2	. . . . . . . . 9 |- B e. _V
5	1, 4	opi1 4669	. . . . . . . 8 |- { A } e. <. A , B >.
6		id 22	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
7	5, 6	syl5eleq 2535	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
8		oprcl 4191	. . . . . . 7 |- ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )
9	7, 8	syl 17	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> ( C e. _V /\ D e. _V ) )
10	9	simpld 461	. . . . 5 |- ( <. A , B >. = <. C , D >. -> C e. _V )
11		prid1g 4078	. . . . 5 |- ( C e. _V -> C e. { C , D } )
12	10, 11	syl 17	. . . 4 |- ( <. A , B >. = <. C , D >. -> C e. { C , D } )
13		eleq2 2518	. . . 4 |- ( { A } = { C , D } -> ( C e. { A } <-> C e. { C , D } ) )
14	12, 13	syl5ibrcom 226	. . 3 |- ( <. A , B >. = <. C , D >. -> ( { A } = { C , D } -> C e. { A } ) )
15		elsni 3993	. . . 4 |- ( C e. { A } -> C = A )
16	15	eqcomd 2457	. . 3 |- ( C e. { A } -> A = C )
17	14, 16	syl6 34	. 2 |- ( <. A , B >. = <. C , D >. -> ( { A } = { C , D } -> A = C ) )
18		dfopg 4164	. . . . 5 |- ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )
19	7, 8, 18	3syl 18	. . . 4 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , D } } )
20	7, 19	eleqtrd 2531	. . 3 |- ( <. A , B >. = <. C , D >. -> { A } e. { { C } , { C , D } } )
21		elpri 3985	. . 3 |- ( { A } e. { { C } , { C , D } } -> ( { A } = { C } \/ { A } = { C , D } ) )
22	20, 21	syl 17	. 2 |- ( <. A , B >. = <. C , D >. -> ( { A } = { C } \/ { A } = { C , D } ) )
23	3, 17, 22	mpjaod 383	1 |- ( <. A , B >. = <. C , D >. -> A = C )

Syntax hints:   -> wi 4   \/ wo 370   /\ wa 371   = wceq 1444   e. wcel 1887   _Vcvv 3045   {csn 3968   {cpr 3970   <.cop 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975

This theorem is referenced by:  opth  4676  dmsnopg  5307  funcnvsn  5627  oprabid  6317  seqomlem2  7168  unxpdomlem3  7778  dfac5lem4  8557  dcomex  8877  canthwelem  9075  uzrdgfni  12172  gsum2d2  17606  2trllemA  25280  2pthon  25332  2pthon3v  25334  constr3lem2  25374  poimirlem9  31949