Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fnssres | Structured version Visualization version GIF version |
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fnssres | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnssresb 5917 | . 2 ⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) | |
2 | 1 | biimpar 501 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊆ wss 3540 ↾ cres 5040 Fn wfn 5799 |
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-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-res 5050 df-fun 5806 df-fn 5807 |
This theorem is referenced by: fnresin1 5919 fnresin2 5920 fssres 5983 fvreseq0 6225 fnreseql 6235 ffvresb 6301 fnressn 6330 soisores 6477 oprres 6700 ofres 6811 fnsuppres 7209 tfrlem1 7359 tz7.48lem 7423 tz7.49c 7428 resixp 7829 ixpfi2 8147 dfac12lem1 8848 ackbij2lem3 8946 cfsmolem 8975 alephsing 8981 ttukeylem3 9216 iunfo 9240 fpwwe2lem8 9338 mulnzcnopr 10552 seqfeq2 12686 seqf1olem2 12703 swrd0len 13274 swrdccat1 13309 bpolylem 14618 reeff1 14689 eucalg 15138 sscres 16306 fullsubc 16333 fullresc 16334 funcres2c 16384 dmaf 16522 cdaf 16523 frmdplusg 17214 frmdss2 17223 gass 17557 dprdfadd 18242 mgpf 18382 prdscrngd 18436 subrgascl 19319 mdetrsca 20228 upxp 21236 uptx 21238 cnmpt1st 21281 cnmpt2nd 21282 cnextfres1 21682 prdstmdd 21737 ressprdsds 21986 prdsxmslem2 22144 xrsdsre 22421 itg1addlem4 23272 recosf1o 24085 resinf1o 24086 dvdsmulf1o 24720 eupath2lem3 26506 sspg 26967 ssps 26969 sspmlem 26971 sspn 26975 hhssnv 27505 1stpreimas 28866 cnre2csqlem 29284 rmulccn 29302 raddcn 29303 carsggect 29707 subiwrdlen 29775 signsvtn0 29973 signstres 29978 bnj1253 30339 bnj1280 30342 subfacp1lem3 30418 subfacp1lem5 30420 cvmlift2lem9a 30539 nodenselem6 31085 filnetlem4 31546 finixpnum 32564 poimirlem4 32583 poimirlem8 32587 ftc1anclem3 32657 isdrngo2 32927 diaintclN 35365 dibintclN 35474 dihintcl 35651 imaiinfv 36274 fnwe2lem2 36639 aomclem6 36647 deg1mhm 36804 resincncf 38760 icccncfext 38773 dvnprodlem1 38836 fourierdlem42 39042 fourierdlem73 39072 pfxccat1 40273 1wlkres 40879 rnghmresfn 41755 rnghmsscmap2 41765 rnghmsscmap 41766 rhmresfn 41801 rhmsscmap2 41811 rhmsscmap 41812 fdivmpt 42132 |
Copyright terms: Public domain | W3C validator |