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

Theorem opth 4390
 Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that and are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)
Hypotheses
Ref Expression
opth1.1
opth1.2
Assertion
Ref Expression
opth

Proof of Theorem opth
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 opth1.1 . . . 4
2 opth1.2 . . . 4
31, 2opth1 4389 . . 3
41, 2opi1 4385 . . . . . . 7
5 id 20 . . . . . . 7
64, 5syl5eleq 2487 . . . . . 6
7 oprcl 3964 . . . . . 6
86, 7syl 16 . . . . 5
98simprd 450 . . . 4
103opeq1d 3946 . . . . . . . 8
1110, 5eqtr3d 2435 . . . . . . 7
128simpld 446 . . . . . . . 8
13 dfopg 3938 . . . . . . . 8
1412, 2, 13sylancl 644 . . . . . . 7
1511, 14eqtr3d 2435 . . . . . 6
16 dfopg 3938 . . . . . . 7
178, 16syl 16 . . . . . 6
1815, 17eqtr3d 2435 . . . . 5
19 prex 4361 . . . . . 6
20 prex 4361 . . . . . 6
2119, 20preqr2 3929 . . . . 5
2218, 21syl 16 . . . 4
23 preq2 3841 . . . . . . 7
2423eqeq2d 2412 . . . . . 6
25 eqeq2 2410 . . . . . 6
2624, 25imbi12d 312 . . . . 5
27 vex 2916 . . . . . 6
282, 27preqr2 3929 . . . . 5
2926, 28vtoclg 2968 . . . 4
309, 22, 29sylc 58 . . 3
313, 30jca 519 . 2
32 opeq12 3942 . 2
3331, 32impbii 181 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1649   wcel 1721  cvv 2913  csn 3771  cpr 3772  cop 3774 This theorem is referenced by:  opthg  4391  otth2  4394  copsexg  4397  copsex4g  4400  opcom  4405  moop2  4406  opelopabsbOLD  4418  ralxpf  4973  cnvcnvsn  5301  funopg  5439  xpopth  6341  eqop  6342  soxp  6409  fnwelem  6411  opiota  6485  xpdom2  7153  xpf1o  7219  unxpdomlem2  7264  unxpdomlem3  7265  xpwdomg  7500  fseqenlem1  7852  iundom2g  8362  eqresr  8959  cnref1o  10553  hashfun  11641  fsumcom2  12499  xpnnenOLD  12750  qredeu  13048  qnumdenbi  13077  crt  13108  prmreclem3  13227  imasaddfnlem  13694  dprd2da  15541  dprd2d2  15543  ucnima  18246  wlkntrllem2  21428  xppreima2  23916  erdszelem9  24678  brtp  25144  br8  25151  br6  25152  br4  25153  elfuns  25492  brsegle  25770  f1opr  26133  pellexlem3  26601  pellex  26605  opelopab4  27997  dib1dim  31296  diclspsn  31325  dihopelvalcpre  31379  dihmeetlem4preN  31437  dihmeetlem13N  31450  dih1dimatlem  31460  dihatlat  31465 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-rab 2672  df-v 2915  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-op 3780
 Copyright terms: Public domain W3C validator