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 5370 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
4 | 1, 2 | opi1 5363 | . . . . . . 7 ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
5 | id 22 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
6 | 4, 5 | eleqtrid 2922 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) |
7 | oprcl 4832 | . . . . . 6 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
8 | 6, 7 | syl 17 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
9 | 8 | simprd 498 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐷 ∈ V) |
10 | 3 | opeq1d 4812 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) |
11 | 10, 5 | eqtr3d 2861 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) |
12 | 8 | simpld 497 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐶 ∈ V) |
13 | dfopg 4804 | . . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) | |
14 | 12, 2, 13 | sylancl 588 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) |
15 | 11, 14 | eqtr3d 2861 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐵}}) |
16 | dfopg 4804 | . . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) | |
17 | 8, 16 | syl 17 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2861 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}}) |
19 | prex 5336 | . . . . . 6 ⊢ {𝐶, 𝐵} ∈ V | |
20 | prex 5336 | . . . . . 6 ⊢ {𝐶, 𝐷} ∈ V | |
21 | 19, 20 | preqr2 4783 | . . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷}) |
22 | 18, 21 | syl 17 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐶, 𝐵} = {𝐶, 𝐷}) |
23 | preq2 4673 | . . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷}) | |
24 | 23 | eqeq2d 2835 | . . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) |
25 | eqeq2 2836 | . . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷)) | |
26 | 24, 25 | imbi12d 347 | . . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))) |
27 | vex 3500 | . . . . . 6 ⊢ 𝑥 ∈ V | |
28 | 2, 27 | preqr2 4783 | . . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) |
29 | 26, 28 | vtoclg 3570 | . . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) |
30 | 9, 22, 29 | sylc 65 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐵 = 𝐷) |
31 | 3, 30 | jca 514 | . 2 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
32 | opeq12 4808 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
33 | 31, 32 | impbii 211 | 1 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1536 ∈ wcel 2113 Vcvv 3497 {csn 4570 {cpr 4572 〈cop 4576 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pr 5333 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 |
This theorem is referenced by: opthg 5372 otth2 5378 copsexgw 5384 copsexg 5385 copsex4g 5388 opcom 5394 moop2 5395 propssopi 5401 opelopabsbALT 5419 ralxpf 5720 cnvcnvsn 6079 opreu2reurex 6148 funopg 6392 funsndifnop 6916 tpres 6966 f1opr 7213 oprabv 7217 xpopth 7733 eqop 7734 opiota 7760 soxp 7826 fnwelem 7828 xpdom2 8615 xpf1o 8682 unxpdomlem2 8726 unxpdomlem3 8727 xpwdomg 9052 djulf1o 9344 djurf1o 9345 fseqenlem1 9453 iundom2g 9965 eqresr 10562 cnref1o 12387 hashfun 13801 fsumcom2 15132 fprodcom2 15341 qredeu 16005 qnumdenbi 16087 crth 16118 prmreclem3 16257 imasaddfnlem 16804 fnpr2ob 16834 dprd2da 19167 dprd2d2 19169 ucnima 22893 numclwwlk1lem2f1 28139 br8d 30364 xppreima2 30398 aciunf1lem 30410 ofpreima 30413 erdszelem9 32450 goeleq12bg 32600 gonanegoal 32603 gonan0 32643 goaln0 32644 gonarlem 32645 gonar 32646 goalrlem 32647 goalr 32648 fmla0disjsuc 32649 fmlasucdisj 32650 satffunlem 32652 satffunlem1lem1 32653 satffunlem2lem1 32655 msubff1 32807 mvhf1 32810 brtp 32989 br8 32996 br6 32997 br4 32998 brsegle 33573 copsex2b 34436 poimirlem4 34900 poimirlem9 34905 dib1dim 38305 diclspsn 38334 dihopelvalcpre 38388 dihmeetlem4preN 38446 dihmeetlem13N 38459 dih1dimatlem 38469 dihatlat 38474 pellexlem3 39434 pellex 39438 snhesn 40138 opelopab4 40891 ichnreuop 43641 ichreuopeq 43642 rrx2xpref1o 44712 |
Copyright terms: Public domain | W3C validator |