Theorem opth1 4537

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
opth1.2

Assertion

Ref	Expression
opth1

Proof of Theorem opth1

Step	Hyp	Ref	Expression
1		opth1.1	. . . 4
2	1	sneqr 4015	. . 3
3	2	a1i 11	. 2
4		opth1.2	. . . . . . . . 9
5	1, 4	opi1 4531	. . . . . . . 8
6		id 21	. . . . . . . 8
7	5, 6	syl5eleq 2508	. . . . . . 7
8		oprcl 4059	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10	9	simpld 449	. . . . 5
11		prid1g 3956	. . . . 5
12	10, 11	syl 16	. . . 4
13		eleq2 2483	. . . 4
14	12, 13	syl5ibrcom 216	. . 3
15		elsni 3879	. . . 4
16	15	eqcomd 2427	. . 3
17	14, 16	syl6 32	. 2
18		dfopg 4032	. . . . 5
19	7, 8, 18	3syl 19	. . . 4
20	7, 19	eleqtrd 2498	. . 3
21		elpri 3874	. . 3
22	20, 21	syl 16	. 2
23	3, 17, 22	mpjaod 374	1

Syntax hints:  ->wi 4  \/wo 361  /\wa 362  =wceq 1687  e.wcel 1749  cvv 2951  {csn 3853  {cpr 3854  <.cop 3856

This theorem is referenced by:  opth  4538  dmsnopg  5282  funcnvsn  5433  oprabid  6085  seqomlem2  6865  unxpdomlem3  7478  dfac5lem4  8243  dcomex  8563  canthwelem  8763  uzrdgfni  11722  gsum2d2  16357  2trllemA  23128  2pthon  23180  2pthon3v  23182  constr3lem2  23211  gsumX2d2  30506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503

This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862