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 3497 | . . . . 5 ⊢ 𝑥 ∈ V | |
2 | 1 | eldm2 5764 | . . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵)) |
3 | 19.42v 1950 | . . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴)) | |
4 | vex 3497 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
5 | 4 | opelresi 5855 | . . . . . 6 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
6 | 5 | exbii 1844 | . . . . 5 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
7 | 1 | eldm2 5764 | . . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
8 | 7 | anbi2i 624 | . . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴)) |
9 | 3, 6, 8 | 3bitr4i 305 | . . . 4 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴)) |
10 | 2, 9 | bitr2i 278 | . . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵)) |
11 | 10 | ineqri 4179 | . 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵) |
12 | 11 | eqcomi 2830 | 1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 = wceq 1533 ∃wex 1776 ∈ wcel 2110 ∩ cin 3934 〈cop 4566 dom cdm 5549 ↾ cres 5551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-br 5059 df-opab 5121 df-xp 5555 df-dm 5559 df-res 5561 |
This theorem is referenced by: ssdmres 5870 dmresexg 5871 dmressnsn 5888 eldmeldmressn 5890 imadisj 5942 imainrect 6032 dmresv 6051 resdmres 6083 coeq0 6102 funimacnv 6429 fnresdisj 6461 fnres 6468 fresaunres2 6544 nfvres 6700 ssimaex 6742 fnreseql 6812 respreima 6830 fveqressseq 6841 ffvresb 6882 fsnunfv 6943 funfvima 6986 funiunfv 7001 offres 7678 fnwelem 7819 ressuppss 7843 ressuppssdif 7845 smores 7983 smores3 7984 smores2 7985 tz7.44-2 8037 tz7.44-3 8038 frfnom 8064 sbthlem5 8625 sbthlem7 8627 domss2 8670 imafi 8811 ordtypelem4 8979 wdomima2g 9044 r0weon 9432 imadomg 9950 dmaddpi 10306 dmmulpi 10307 ltweuz 13323 dmhashres 13695 limsupgle 14828 fvsetsid 16509 setsdm 16511 setsfun 16512 setsfun0 16513 setsres 16519 lubdm 17583 glbdm 17596 gsumzaddlem 19035 dprdcntz2 19154 lmres 21902 imacmp 21999 qtoptop2 22301 kqdisj 22334 metreslem 22966 setsmstopn 23082 ismbl 24121 mbfres 24239 dvres3a 24506 cpnres 24528 dvlipcn 24585 dvlip2 24586 c1lip3 24590 dvcnvrelem1 24608 dvcvx 24611 dvlog 25228 uhgrspansubgrlem 27066 trlsegvdeglem4 27996 hlimcaui 29007 funresdm1 30349 ftc2re 31864 dfrdg2 33035 frrlem11 33128 frrlem12 33129 sltres 33164 nolesgn2ores 33174 nodense 33191 nosupres 33202 nosupbnd1lem1 33203 nosupbnd2lem1 33210 nosupbnd2 33211 bj-fvsnun2 34532 caures 35029 ssbnd 35060 mapfzcons1 39307 diophrw 39349 eldioph2lem1 39350 eldioph2lem2 39351 rp-imass 40110 dmresss 41494 limsupresxr 42040 liminfresxr 42041 fourierdlem93 42478 fouriersw 42510 sssmf 43009 eldmressn 43266 fnresfnco 43270 afvres 43365 afv2res 43432 setrec2lem1 44790 |
Copyright terms: Public domain | W3C validator |