![]() |
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 5477 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
4 | 1, 2 | opi1 5470 | . . . . . . 7 ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
5 | id 22 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
6 | 4, 5 | eleqtrid 2831 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴} ∈ 〈𝐶, 𝐷〉) |
7 | oprcl 4901 | . . . . . 6 ⊢ ({𝐴} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
8 | 6, 7 | syl 17 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
9 | 8 | simprd 494 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐷 ∈ V) |
10 | 3 | opeq1d 4881 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐵〉) |
11 | 10, 5 | eqtr3d 2767 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = 〈𝐶, 𝐷〉) |
12 | 8 | simpld 493 | . . . . . . . 8 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐶 ∈ V) |
13 | dfopg 4873 | . . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) | |
14 | 12, 2, 13 | sylancl 584 | . . . . . . 7 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐵〉 = {{𝐶}, {𝐶, 𝐵}}) |
15 | 11, 14 | eqtr3d 2767 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐵}}) |
16 | dfopg 4873 | . . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) | |
17 | 8, 16 | syl 17 | . . . . . 6 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2767 | . . . . 5 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}}) |
19 | prex 5434 | . . . . . 6 ⊢ {𝐶, 𝐵} ∈ V | |
20 | prex 5434 | . . . . . 6 ⊢ {𝐶, 𝐷} ∈ V | |
21 | 19, 20 | preqr2 4852 | . . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷}) |
22 | 18, 21 | syl 17 | . . . 4 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐶, 𝐵} = {𝐶, 𝐷}) |
23 | preq2 4740 | . . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷}) | |
24 | 23 | eqeq2d 2736 | . . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) |
25 | eqeq2 2737 | . . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷)) | |
26 | 24, 25 | imbi12d 343 | . . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))) |
27 | vex 3465 | . . . . . 6 ⊢ 𝑥 ∈ V | |
28 | 2, 27 | preqr2 4852 | . . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) |
29 | 26, 28 | vtoclg 3532 | . . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) |
30 | 9, 22, 29 | sylc 65 | . . 3 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐵 = 𝐷) |
31 | 3, 30 | jca 510 | . 2 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
32 | opeq12 4877 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | |
33 | 31, 32 | impbii 208 | 1 ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∈ wcel 2098 Vcvv 3461 {csn 4630 {cpr 4632 〈cop 4636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 |
This theorem is referenced by: opthg 5479 otth2 5485 copsexgw 5492 copsexg 5493 copsex2g 5495 copsex4g 5497 opcom 5503 moop2 5504 propssopi 5510 brtp 5525 vopelopabsb 5531 ralxpf 5849 cnvopab 6144 cnvcnvsn 6225 opreu2reurex 6300 funopg 6588 funsndifnop 7160 tpres 7213 f1opr 7476 oprabv 7480 xpopth 8035 eqop 8036 opiota 8064 soxp 8134 fnwelem 8136 xpdom2 9092 xpf1o 9164 unxpdomlem2 9276 unxpdomlem3 9277 xpwdomg 9610 djulf1o 9937 djurf1o 9938 fseqenlem1 10049 iundom2g 10565 eqresr 11162 cnref1o 13002 hashfun 14432 fsumcom2 15756 fprodcom2 15964 qredeu 16632 qnumdenbi 16719 crth 16750 prmreclem3 16890 imasaddfnlem 17513 fnpr2ob 17543 dprd2da 20011 dprd2d2 20013 rngqiprngimf1 21207 ucnima 24230 numclwwlk1lem2f1 30239 brab2d 32476 br8d 32479 xppreima2 32518 aciunf1lem 32529 ofpreima 32532 erdszelem9 34937 goeleq12bg 35087 gonanegoal 35090 gonan0 35130 goaln0 35131 gonarlem 35132 gonar 35133 goalrlem 35134 goalr 35135 fmla0disjsuc 35136 fmlasucdisj 35137 satffunlem 35139 satffunlem1lem1 35140 satffunlem2lem1 35142 msubff1 35294 mvhf1 35297 br8 35478 br6 35479 br4 35480 brsegle 35832 copsex2b 36747 poimirlem4 37225 poimirlem9 37230 dib1dim 40765 diclspsn 40794 dihopelvalcpre 40848 dihmeetlem4preN 40906 dihmeetlem13N 40919 dih1dimatlem 40929 dihatlat 40934 pellexlem3 42390 pellex 42394 snhesn 43355 opelopab4 44129 ichnreuop 46946 ichreuopeq 46947 rrx2xpref1o 47974 |
Copyright terms: Public domain | W3C validator |