Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opth | Structured version Visualization version Unicode version |
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.) |
Ref | Expression |
---|---|
opth1.1 | |
opth1.2 |
Ref | Expression |
---|---|
opth |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opth1.1 | . . . 4 | |
2 | opth1.2 | . . . 4 | |
3 | 1, 2 | opth1 4944 | . . 3 |
4 | 1, 2 | opi1 4937 | . . . . . . 7 |
5 | id 22 | . . . . . . 7 | |
6 | 4, 5 | syl5eleq 2707 | . . . . . 6 |
7 | oprcl 4427 | . . . . . 6 | |
8 | 6, 7 | syl 17 | . . . . 5 |
9 | 8 | simprd 479 | . . . 4 |
10 | 3 | opeq1d 4408 | . . . . . . . 8 |
11 | 10, 5 | eqtr3d 2658 | . . . . . . 7 |
12 | 8 | simpld 475 | . . . . . . . 8 |
13 | dfopg 4400 | . . . . . . . 8 | |
14 | 12, 2, 13 | sylancl 694 | . . . . . . 7 |
15 | 11, 14 | eqtr3d 2658 | . . . . . 6 |
16 | dfopg 4400 | . . . . . . 7 | |
17 | 8, 16 | syl 17 | . . . . . 6 |
18 | 15, 17 | eqtr3d 2658 | . . . . 5 |
19 | prex 4909 | . . . . . 6 | |
20 | prex 4909 | . . . . . 6 | |
21 | 19, 20 | preqr2 4381 | . . . . 5 |
22 | 18, 21 | syl 17 | . . . 4 |
23 | preq2 4269 | . . . . . . 7 | |
24 | 23 | eqeq2d 2632 | . . . . . 6 |
25 | eqeq2 2633 | . . . . . 6 | |
26 | 24, 25 | imbi12d 334 | . . . . 5 |
27 | vex 3203 | . . . . . 6 | |
28 | 2, 27 | preqr2 4381 | . . . . 5 |
29 | 26, 28 | vtoclg 3266 | . . . 4 |
30 | 9, 22, 29 | sylc 65 | . . 3 |
31 | 3, 30 | jca 554 | . 2 |
32 | opeq12 4404 | . 2 | |
33 | 31, 32 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wcel 1990 cvv 3200 csn 4177 cpr 4179 cop 4183 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 |
This theorem is referenced by: opthg 4946 otth2 4952 copsexg 4956 copsex4g 4959 opcom 4965 moop2 4966 propssopi 4971 opelopabsbALT 4984 ralxpf 5268 cnvcnvsn 5612 funopg 5922 funsndifnop 6416 tpres 6466 oprabv 6703 xpopth 7207 eqop 7208 opiota 7229 soxp 7290 fnwelem 7292 xpdom2 8055 xpf1o 8122 unxpdomlem2 8165 unxpdomlem3 8166 xpwdomg 8490 fseqenlem1 8847 iundom2g 9362 eqresr 9958 cnref1o 11827 hashfun 13224 fsumcom2 14505 fsumcom2OLD 14506 fprodcom2 14714 fprodcom2OLD 14715 qredeu 15372 qnumdenbi 15452 crth 15483 prmreclem3 15622 imasaddfnlem 16188 dprd2da 18441 dprd2d2 18443 ucnima 22085 numclwlk1lem2f1 27227 br8d 29422 xppreima2 29450 aciunf1lem 29462 ofpreima 29465 erdszelem9 31181 msubff1 31453 mvhf1 31456 brtp 31639 br8 31646 br6 31647 br4 31648 brsegle 32215 poimirlem4 33413 poimirlem9 33418 f1opr 33519 dib1dim 36454 diclspsn 36483 dihopelvalcpre 36537 dihmeetlem4preN 36595 dihmeetlem13N 36608 dih1dimatlem 36618 dihatlat 36623 pellexlem3 37395 pellex 37399 snhesn 38080 opelopab4 38767 |
Copyright terms: Public domain | W3C validator |