![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmres | Structured version Visualization version GIF version |
Description: The domain of a restriction. Exercise 14 of [TakeutiZaring] p. 25. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
dmres | ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3465 | . . . . 5 ⊢ 𝑥 ∈ V | |
2 | 1 | eldm2 5907 | . . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵)) |
3 | 19.42v 1949 | . . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴)) | |
4 | vex 3465 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
5 | 4 | opelresi 5996 | . . . . . 6 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
6 | 5 | exbii 1842 | . . . . 5 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
7 | 1 | eldm2 5907 | . . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
8 | 7 | anbi2i 621 | . . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴)) |
9 | 3, 6, 8 | 3bitr4i 302 | . . . 4 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴)) |
10 | 2, 9 | bitr2i 275 | . . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵)) |
11 | 10 | ineqri 4204 | . 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵) |
12 | 11 | eqcomi 2734 | 1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∩ cin 3945 〈cop 4638 dom cdm 5681 ↾ cres 5683 |
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 5303 ax-nul 5310 ax-pr 5432 |
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-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4325 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-br 5153 df-opab 5215 df-xp 5687 df-dm 5691 df-res 5693 |
This theorem is referenced by: ssdmres 6021 dmresexg 6022 dmressnsn 6031 eldmeldmressn 6033 relresdm1 6041 imadisj 6088 imainrect 6191 dmresv 6210 resdmres 6242 resdmss 6245 coeq0 6265 resssxp 6280 snres0 6308 funimacnv 6639 fnresdisj 6680 fnres 6687 fresaunres2 6773 nfvres 6941 ssimaex 6986 fnreseql 7060 respreima 7078 fveqressseq 7092 ffvresb 7138 fsnunfv 7200 funfvima 7246 funiunfv 7262 offres 7996 fnwelem 8144 ressuppss 8196 ressuppssdif 8198 frrlem11 8310 frrlem12 8311 smores 8381 smores3 8382 smores2 8383 tz7.44-2 8436 tz7.44-3 8437 frfnom 8464 sbthlem5 9124 sbthlem7 9126 domss2 9173 imafiALT 9385 ordtypelem4 9560 wdomima2g 9625 r0weon 10051 imadomg 10573 dmaddpi 10929 dmmulpi 10930 ltweuz 13976 dmhashres 14353 limsupgle 15474 fvsetsid 17165 setsdm 17167 setsfun 17168 setsfun0 17169 setsres 17175 lubdm 18371 glbdm 18384 gsumzaddlem 19914 dprdcntz2 20033 lmres 23287 imacmp 23384 qtoptop2 23686 kqdisj 23719 metreslem 24351 setsmstopn 24469 ismbl 25538 mbfres 25656 dvres3a 25926 cpnres 25950 dvlipcn 26010 dvlip2 26011 c1lip3 26015 dvcnvrelem1 26033 dvcvx 26036 dvlog 26670 sltres 27684 nolesgn2ores 27694 nogesgn1ores 27696 nodense 27714 nosupres 27729 nosupbnd1lem1 27730 nosupbnd2lem1 27737 nosupbnd2 27738 noinfres 27744 noinfbnd1lem1 27745 noinfbnd2lem1 27752 noetasuplem2 27756 noetainflem2 27760 uhgrspansubgrlem 29218 trlsegvdeglem4 30148 hlimcaui 31161 ftc2re 34400 dfrdg2 35567 bj-fvsnun2 36911 caures 37409 ssbnd 37437 mapfzcons1 42311 diophrw 42353 eldioph2lem1 42354 eldioph2lem2 42355 tfsconcatrev 42951 limsupresxr 45324 liminfresxr 45325 fourierdlem93 45757 fouriersw 45789 sssmf 46296 eldmressn 46589 fnresfnco 46593 afvres 46722 afv2res 46789 |
Copyright terms: Public domain | W3C validator |