Theorem opth1 4682

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 4157	. . 3
3	2	a1i 11	. 2
4		opth1.2	. . . . . . . . 9
5	1, 4	opi1 4676	. . . . . . . 8
6		id 22	. . . . . . . 8
7	5, 6	syl5eleq 2548	. . . . . . 7
8		oprcl 4201	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10	9	simpld 459	. . . . 5
11		prid1g 4098	. . . . 5
12	10, 11	syl 16	. . . 4
13		eleq2 2527	. . . 4
14	12, 13	syl5ibrcom 222	. . 3
15		elsni 4018	. . . 4
16	15	eqcomd 2462	. . 3
17	14, 16	syl6 33	. 2
18		dfopg 4174	. . . . 5
19	7, 8, 18	3syl 20	. . . 4
20	7, 19	eleqtrd 2544	. . 3
21		elpri 4013	. . 3
22	20, 21	syl 16	. 2
23	3, 17, 22	mpjaod 381	1

Syntax hints:  ->wi 4  \/wo 368  /\wa 369  =wceq 1370  e.wcel 1758  cvv 3081  {csn 3993  {cpr 3995  <.cop 3999

This theorem is referenced by:  opth  4683  dmsnopg  5429  funcnvsn  5582  oprabid  6246  seqomlem2  7040  unxpdomlem3  7654  dfac5lem4  8433  dcomex  8753  canthwelem  8954  uzrdgfni  11926  gsum2d2  16635  2trllemA  23918  2pthon  23970  2pthon3v  23972  constr3lem2  24001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pr 4648

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000