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

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
StepHypRef Expression
1 opth1.1 . . . 4
21sneqr 4157 . . 3
32a1i 11 . 2
4 opth1.2 . . . . . . . . 9
51, 4opi1 4676 . . . . . . . 8
6 id 22 . . . . . . . 8
75, 6syl5eleq 2548 . . . . . . 7
8 oprcl 4201 . . . . . . 7
97, 8syl 16 . . . . . 6
109simpld 459 . . . . 5
11 prid1g 4098 . . . . 5
1210, 11syl 16 . . . 4
13 eleq2 2527 . . . 4
1412, 13syl5ibrcom 222 . . 3
15 elsni 4018 . . . 4
1615eqcomd 2462 . . 3
1714, 16syl6 33 . 2
18 dfopg 4174 . . . . 5
197, 8, 183syl 20 . . . 4
207, 19eleqtrd 2544 . . 3
21 elpri 4013 . . 3
2220, 21syl 16 . 2
233, 17, 22mpjaod 381 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator