Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssdmres | Structured version Visualization version GIF version |
Description: A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.) |
Ref | Expression |
---|---|
ssdmres | ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ss 3904 | . 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴) | |
2 | dmres 5913 | . . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵) | |
3 | 2 | eqeq1i 2743 | . 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴) |
4 | 1, 3 | bitr4i 277 | 1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1539 ∩ cin 3886 ⊆ wss 3887 dom cdm 5589 ↾ cres 5591 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-xp 5595 df-dm 5599 df-res 5601 |
This theorem is referenced by: dmresi 5961 fnssresb 6554 fores 6698 foimacnv 6733 dffv2 6863 sbthlem4 8873 hashres 14153 hashimarn 14155 dvres3 25077 c1liplem1 25160 lhop1lem 25177 lhop 25180 usgrres 27675 vtxdginducedm1lem2 27907 wlkres 28038 trlreslem 28067 hhssabloi 29624 hhssnv 29626 hhshsslem1 29629 fresf1o 30966 fsupprnfi 31026 gsumhashmul 31316 cycpmconjvlem 31408 exidreslem 36035 divrngcl 36115 isdrngo2 36116 n0elqs2 36462 dvbdfbdioolem1 43469 fourierdlem48 43695 fourierdlem49 43696 fourierdlem71 43718 fourierdlem73 43720 fourierdlem94 43741 fourierdlem111 43758 fourierdlem112 43759 fourierdlem113 43760 fouriersw 43772 fouriercn 43773 dmvon 44144 |
Copyright terms: Public domain | W3C validator |