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 3860 | . 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴) | |
2 | dmres 5847 | . . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵) | |
3 | 2 | eqeq1i 2743 | . 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴) |
4 | 1, 3 | bitr4i 281 | 1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1542 ∩ cin 3842 ⊆ wss 3843 dom cdm 5525 ↾ cres 5527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-v 3400 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-br 5031 df-opab 5093 df-xp 5531 df-dm 5535 df-res 5537 |
This theorem is referenced by: dmresi 5895 fnssresb 6458 fores 6602 foimacnv 6635 dffv2 6763 sbthlem4 8680 hashres 13891 hashimarn 13893 dvres3 24665 c1liplem1 24748 lhop1lem 24765 lhop 24768 usgrres 27250 vtxdginducedm1lem2 27482 wlkres 27612 trlreslem 27641 hhssabloi 29197 hhssnv 29199 hhshsslem1 29202 fresf1o 30540 fsupprnfi 30601 gsumhashmul 30893 cycpmconjvlem 30985 exidreslem 35658 divrngcl 35738 isdrngo2 35739 n0elqs2 36085 dvbdfbdioolem1 43011 fourierdlem48 43237 fourierdlem49 43238 fourierdlem71 43260 fourierdlem73 43262 fourierdlem94 43283 fourierdlem111 43300 fourierdlem112 43301 fourierdlem113 43302 fouriersw 43314 fouriercn 43315 dmvon 43686 |
Copyright terms: Public domain | W3C validator |