![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opth | Structured version Visualization version GIF 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 | ⊢ 𝐴 ∈ V |
opth1.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
opth | ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opth1.1 | . . . 4 ⊢ 𝐴 ∈ V | |
2 | opth1.2 | . . . 4 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | opth1 5175 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
4 | 1, 2 | opi1 5168 | . . . . . . 7 ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
5 | id 22 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
6 | 4, 5 | syl5eleq 2864 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) |
7 | oprcl 4662 | . . . . . 6 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
8 | 6, 7 | syl 17 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
9 | 8 | simprd 491 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐷 ∈ V) |
10 | 3 | opeq1d 4642 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) |
11 | 10, 5 | eqtr3d 2815 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) |
12 | 8 | simpld 490 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐶 ∈ V) |
13 | dfopg 4634 | . . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) | |
14 | 12, 2, 13 | sylancl 580 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) |
15 | 11, 14 | eqtr3d 2815 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐵}}) |
16 | dfopg 4634 | . . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) | |
17 | 8, 16 | syl 17 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2815 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}}) |
19 | prex 5141 | . . . . . 6 ⊢ {𝐶, 𝐵} ∈ V | |
20 | prex 5141 | . . . . . 6 ⊢ {𝐶, 𝐷} ∈ V | |
21 | 19, 20 | preqr2 4609 | . . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷}) |
22 | 18, 21 | syl 17 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐶, 𝐵} = {𝐶, 𝐷}) |
23 | preq2 4500 | . . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷}) | |
24 | 23 | eqeq2d 2787 | . . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) |
25 | eqeq2 2788 | . . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷)) | |
26 | 24, 25 | imbi12d 336 | . . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))) |
27 | vex 3400 | . . . . . 6 ⊢ 𝑥 ∈ V | |
28 | 2, 27 | preqr2 4609 | . . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) |
29 | 26, 28 | vtoclg 3466 | . . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) |
30 | 9, 22, 29 | sylc 65 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐵 = 𝐷) |
31 | 3, 30 | jca 507 | . 2 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
32 | opeq12 4638 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
33 | 31, 32 | impbii 201 | 1 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∈ wcel 2106 Vcvv 3397 {csn 4397 {cpr 4399 〈cop 4403 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-rab 3098 df-v 3399 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-nul 4141 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 |
This theorem is referenced by: opthg 5177 otth2 5183 copsexg 5187 copsex4g 5190 opcom 5196 moop2 5197 propssopi 5205 opelopabsbALT 5221 ralxpf 5514 cnvcnvsn 5866 funopg 6169 funsndifnop 6682 tpres 6738 oprabv 6980 xpopth 7486 eqop 7487 opiota 7508 soxp 7571 fnwelem 7573 xpdom2 8343 xpf1o 8410 unxpdomlem2 8453 unxpdomlem3 8454 xpwdomg 8779 djulf1o 9071 djurf1o 9072 fseqenlem1 9180 iundom2g 9697 eqresr 10294 cnref1o 12132 hashfun 13538 fsumcom2 14910 fprodcom2 15117 qredeu 15777 qnumdenbi 15856 crth 15887 prmreclem3 16026 imasaddfnlem 16574 dprd2da 18828 dprd2d2 18830 ucnima 22493 numclwwlk1lem2f1 27773 numclwwlk1lem2f1OLD 27778 br8d 29985 xppreima2 30015 aciunf1lem 30027 ofpreima 30030 erdszelem9 31780 msubff1 32052 mvhf1 32055 brtp 32233 br8 32240 br6 32241 br4 32242 brsegle 32804 poimirlem4 34023 poimirlem9 34028 f1opr 34128 dib1dim 37303 diclspsn 37332 dihopelvalcpre 37386 dihmeetlem4preN 37444 dihmeetlem13N 37457 dih1dimatlem 37467 dihatlat 37472 pellexlem3 38337 pellex 38341 snhesn 39018 opelopab4 39693 rrx2xpref1o 43436 |
Copyright terms: Public domain | W3C validator |