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 3176 | . . . . 5 ⊢ 𝑥 ∈ V | |
2 | 1 | eldm2 5244 | . . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵)) |
3 | 19.41v 1901 | . . . . 5 ⊢ (∃𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | vex 3176 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
5 | 4 | opelres 5322 | . . . . . 6 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ (〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
6 | 5 | exbii 1764 | . . . . 5 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
7 | 1 | eldm2 5244 | . . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
8 | 7 | anbi1i 727 | . . . . 5 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
9 | 3, 6, 8 | 3bitr4i 291 | . . . 4 ⊢ (∃𝑦〈𝑥, 𝑦〉 ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵)) |
10 | 2, 9 | bitr2i 264 | . . 3 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵)) |
11 | 10 | ineqri 3768 | . 2 ⊢ (dom 𝐴 ∩ 𝐵) = dom (𝐴 ↾ 𝐵) |
12 | incom 3767 | . 2 ⊢ (dom 𝐴 ∩ 𝐵) = (𝐵 ∩ dom 𝐴) | |
13 | 11, 12 | eqtr3i 2634 | 1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∩ cin 3539 〈cop 4131 dom cdm 5038 ↾ cres 5040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-xp 5044 df-dm 5048 df-res 5050 |
This theorem is referenced by: ssdmres 5340 dmresexg 5341 dmressnsn 5358 eldmeldmressn 5360 imadisj 5403 imainrect 5494 dmresv 5511 resdmres 5543 coeq0 5561 funimacnv 5884 fnresdisj 5915 fnres 5921 fresaunres2 5989 nfvres 6134 ssimaex 6173 fnreseql 6235 respreima 6252 fveqressseq 6263 ffvresb 6301 fsnunfv 6358 funfvima 6396 funiunfv 6410 offres 7054 fnwelem 7179 ressuppss 7201 ressuppssdif 7203 smores 7336 smores3 7337 smores2 7338 tz7.44-2 7390 tz7.44-3 7391 frfnom 7417 sbthlem5 7959 sbthlem7 7961 domss2 8004 imafi 8142 ordtypelem4 8309 wdomima2g 8374 r0weon 8718 imadomg 9237 dmaddpi 9591 dmmulpi 9592 ltweuz 12622 dmhashres 12991 limsupgle 14056 fvsetsid 15722 setsdm 15724 setsfun 15725 setsfun0 15726 setsres 15729 lubdm 16802 glbdm 16815 gsumzaddlem 18144 dprdcntz2 18260 lmres 20914 imacmp 21010 qtoptop2 21312 kqdisj 21345 metreslem 21977 setsmstopn 22093 ismbl 23101 mbfres 23217 dvres3a 23484 cpnres 23506 dvlipcn 23561 dvlip2 23562 c1lip3 23566 dvcnvrelem1 23584 dvcvx 23587 dvlog 24197 cusgrasizeindslem1 26002 eupares 26502 hlimcaui 27477 dfrdg2 30945 sltres 31061 nodense 31088 nofulllem5 31105 caures 32726 ssbnd 32757 mapfzcons1 36298 diophrw 36340 eldioph2lem1 36341 eldioph2lem2 36342 rp-imass 37085 fourierdlem93 39092 fouriersw 39124 sssmf 39625 eldmressn 39852 fnresfnco 39855 afvres 39901 uhgrspansubgrlem 40514 1wlkres 40879 trlsegvdeglem4 41391 setrec2lem1 42239 |
Copyright terms: Public domain | W3C validator |