![]() |
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 5476 | . . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶) |
4 | 1, 2 | opi1 5469 | . . . . . . 7 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩ |
5 | id 22 | . . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩) | |
6 | 4, 5 | eleqtrid 2840 | . . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩) |
7 | oprcl 4900 | . . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | |
8 | 6, 7 | syl 17 | . . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V)) |
9 | 8 | simprd 497 | . . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐷 ∈ V) |
10 | 3 | opeq1d 4880 | . . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐵⟩) |
11 | 10, 5 | eqtr3d 2775 | . . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = ⟨𝐶, 𝐷⟩) |
12 | 8 | simpld 496 | . . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V) |
13 | dfopg 4872 | . . . . . . . 8 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}}) | |
14 | 12, 2, 13 | sylancl 587 | . . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐵⟩ = {{𝐶}, {𝐶, 𝐵}}) |
15 | 11, 14 | eqtr3d 2775 | . . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐵}}) |
16 | dfopg 4872 | . . . . . . 7 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}}) | |
17 | 8, 16 | syl 17 | . . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2775 | . . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}}) |
19 | prex 5433 | . . . . . 6 ⊢ {𝐶, 𝐵} ∈ V | |
20 | prex 5433 | . . . . . 6 ⊢ {𝐶, 𝐷} ∈ V | |
21 | 19, 20 | preqr2 4851 | . . . . 5 ⊢ ({{𝐶}, {𝐶, 𝐵}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, 𝐵} = {𝐶, 𝐷}) |
22 | 18, 21 | syl 17 | . . . 4 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐶, 𝐵} = {𝐶, 𝐷}) |
23 | preq2 4739 | . . . . . . 7 ⊢ (𝑥 = 𝐷 → {𝐶, 𝑥} = {𝐶, 𝐷}) | |
24 | 23 | eqeq2d 2744 | . . . . . 6 ⊢ (𝑥 = 𝐷 → ({𝐶, 𝐵} = {𝐶, 𝑥} ↔ {𝐶, 𝐵} = {𝐶, 𝐷})) |
25 | eqeq2 2745 | . . . . . 6 ⊢ (𝑥 = 𝐷 → (𝐵 = 𝑥 ↔ 𝐵 = 𝐷)) | |
26 | 24, 25 | imbi12d 345 | . . . . 5 ⊢ (𝑥 = 𝐷 → (({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) ↔ ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷))) |
27 | vex 3479 | . . . . . 6 ⊢ 𝑥 ∈ V | |
28 | 2, 27 | preqr2 4851 | . . . . 5 ⊢ ({𝐶, 𝐵} = {𝐶, 𝑥} → 𝐵 = 𝑥) |
29 | 26, 28 | vtoclg 3557 | . . . 4 ⊢ (𝐷 ∈ V → ({𝐶, 𝐵} = {𝐶, 𝐷} → 𝐵 = 𝐷)) |
30 | 9, 22, 29 | sylc 65 | . . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐵 = 𝐷) |
31 | 3, 30 | jca 513 | . 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
32 | opeq12 4876 | . 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩) | |
33 | 31, 32 | impbii 208 | 1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 Vcvv 3475 {csn 4629 {cpr 4631 ⟨cop 4635 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 |
This theorem is referenced by: opthg 5478 otth2 5484 copsexgw 5491 copsexg 5492 copsex2g 5494 copsex4g 5496 opcom 5502 moop2 5503 propssopi 5509 brtp 5524 vopelopabsb 5530 ralxpf 5847 cnvcnvsn 6219 opreu2reurex 6294 funopg 6583 funsndifnop 7149 tpres 7202 f1opr 7465 oprabv 7469 xpopth 8016 eqop 8017 opiota 8045 soxp 8115 fnwelem 8117 xpdom2 9067 xpf1o 9139 unxpdomlem2 9251 unxpdomlem3 9252 xpwdomg 9580 djulf1o 9907 djurf1o 9908 fseqenlem1 10019 iundom2g 10535 eqresr 11132 cnref1o 12969 hashfun 14397 fsumcom2 15720 fprodcom2 15928 qredeu 16595 qnumdenbi 16680 crth 16711 prmreclem3 16851 imasaddfnlem 17474 fnpr2ob 17504 dprd2da 19912 dprd2d2 19914 ucnima 23786 numclwwlk1lem2f1 29610 br8d 31839 xppreima2 31876 aciunf1lem 31887 ofpreima 31890 erdszelem9 34190 goeleq12bg 34340 gonanegoal 34343 gonan0 34383 goaln0 34384 gonarlem 34385 gonar 34386 goalrlem 34387 goalr 34388 fmla0disjsuc 34389 fmlasucdisj 34390 satffunlem 34392 satffunlem1lem1 34393 satffunlem2lem1 34395 msubff1 34547 mvhf1 34550 br8 34726 br6 34727 br4 34728 brsegle 35080 copsex2b 36021 poimirlem4 36492 poimirlem9 36497 dib1dim 40036 diclspsn 40065 dihopelvalcpre 40119 dihmeetlem4preN 40177 dihmeetlem13N 40190 dih1dimatlem 40200 dihatlat 40205 pellexlem3 41569 pellex 41573 snhesn 42537 opelopab4 43312 ichnreuop 46140 ichreuopeq 46141 rngqiprngimf1 46785 rrx2xpref1o 47404 |
Copyright terms: Public domain | W3C validator |