![]() |
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 5332 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
4 | 1, 2 | opi1 5325 | . . . . . . 7 ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
5 | id 22 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
6 | 4, 5 | eleqtrid 2896 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) |
7 | oprcl 4791 | . . . . . 6 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
8 | 6, 7 | syl 17 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
9 | 8 | simprd 499 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐷 ∈ V) |
10 | 3 | opeq1d 4771 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) |
11 | 10, 5 | eqtr3d 2835 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) |
12 | 8 | simpld 498 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐶 ∈ V) |
13 | dfopg 4761 | . . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) | |
14 | 12, 2, 13 | sylancl 589 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) |
15 | 11, 14 | eqtr3d 2835 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐵}}) |
16 | dfopg 4761 | . . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) | |
17 | 8, 16 | syl 17 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2835 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}}) |
19 | prex 5298 | . . . . . 6 ⊢ {𝐶, 𝐵} ∈ V | |
20 | prex 5298 | . . . . . 6 ⊢ {𝐶, 𝐷} ∈ V | |
21 | 19, 20 | preqr2 4740 | . . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷}) |
22 | 18, 21 | syl 17 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐶, 𝐵} = {𝐶, 𝐷}) |
23 | preq2 4630 | . . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷}) | |
24 | 23 | eqeq2d 2809 | . . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) |
25 | eqeq2 2810 | . . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷)) | |
26 | 24, 25 | imbi12d 348 | . . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))) |
27 | vex 3444 | . . . . . 6 ⊢ 𝑥 ∈ V | |
28 | 2, 27 | preqr2 4740 | . . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) |
29 | 26, 28 | vtoclg 3515 | . . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) |
30 | 9, 22, 29 | sylc 65 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐵 = 𝐷) |
31 | 3, 30 | jca 515 | . 2 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
32 | opeq12 4767 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
33 | 31, 32 | impbii 212 | 1 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 Vcvv 3441 {csn 4525 {cpr 4527 〈cop 4531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 |
This theorem is referenced by: opthg 5334 otth2 5340 copsexgw 5346 copsexg 5347 copsex4g 5350 opcom 5356 moop2 5357 propssopi 5363 opelopabsbALT 5381 ralxpf 5681 cnvcnvsn 6043 opreu2reurex 6113 funopg 6358 funsndifnop 6890 tpres 6940 f1opr 7189 oprabv 7193 xpopth 7712 eqop 7713 opiota 7739 soxp 7806 fnwelem 7808 xpdom2 8595 xpf1o 8663 unxpdomlem2 8707 unxpdomlem3 8708 xpwdomg 9033 djulf1o 9325 djurf1o 9326 fseqenlem1 9435 iundom2g 9951 eqresr 10548 cnref1o 12372 hashfun 13794 fsumcom2 15121 fprodcom2 15330 qredeu 15992 qnumdenbi 16074 crth 16105 prmreclem3 16244 imasaddfnlem 16793 fnpr2ob 16823 dprd2da 19157 dprd2d2 19159 ucnima 22887 numclwwlk1lem2f1 28142 br8d 30374 xppreima2 30413 aciunf1lem 30425 ofpreima 30428 erdszelem9 32559 goeleq12bg 32709 gonanegoal 32712 gonan0 32752 goaln0 32753 gonarlem 32754 gonar 32755 goalrlem 32756 goalr 32757 fmla0disjsuc 32758 fmlasucdisj 32759 satffunlem 32761 satffunlem1lem1 32762 satffunlem2lem1 32764 msubff1 32916 mvhf1 32919 brtp 33098 br8 33105 br6 33106 br4 33107 brsegle 33682 copsex2b 34555 poimirlem4 35061 poimirlem9 35066 dib1dim 38461 diclspsn 38490 dihopelvalcpre 38544 dihmeetlem4preN 38602 dihmeetlem13N 38615 dih1dimatlem 38625 dihatlat 38630 pellexlem3 39772 pellex 39776 snhesn 40487 opelopab4 41257 ichnreuop 43989 ichreuopeq 43990 rrx2xpref1o 45132 |
Copyright terms: Public domain | W3C validator |