MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opth1 Unicode version

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
StepHypRef Expression
1 opth1.1 . . . 4
21sneqr 4015 . . 3
32a1i 11 . 2
4 opth1.2 . . . . . . . . 9
51, 4opi1 4531 . . . . . . . 8
6 id 21 . . . . . . . 8
75, 6syl5eleq 2508 . . . . . . 7
8 oprcl 4059 . . . . . . 7
97, 8syl 16 . . . . . 6
109simpld 449 . . . . 5
11 prid1g 3956 . . . . 5
1210, 11syl 16 . . . 4
13 eleq2 2483 . . . 4
1412, 13syl5ibrcom 216 . . 3
15 elsni 3879 . . . 4
1615eqcomd 2427 . . 3
1714, 16syl6 32 . 2
18 dfopg 4032 . . . . 5
197, 8, 183syl 19 . . . 4
207, 19eleqtrd 2498 . . 3
21 elpri 3874 . . 3
2220, 21syl 16 . 2
233, 17, 22mpjaod 374 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator