![]() |
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 6672 | . 2 ⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) | |
2 | 1 | biimpar 477 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3948 ↾ cres 5678 Fn wfn 6538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-res 5688 df-fun 6545 df-fn 6546 |
This theorem is referenced by: fnssresd 6674 fnresin1 6675 fnresin2 6676 fnresi 6679 fssres 6757 fvreseq0 7039 fnreseql 7049 ffvresb 7126 fnressn 7158 soisores 7327 oprres 7579 ofres 7693 fsplitfpar 8109 fnsuppres 8181 tfrlem1 8382 tz7.48lem 8447 tz7.49c 8452 resixp 8933 ixpfi2 9356 ttrclss 9721 dfac12lem1 10144 ackbij2lem3 10242 cfsmolem 10271 alephsing 10277 ttukeylem3 10512 iunfo 10540 fpwwe2lem7 10638 mulnzcnf 11867 seqfeq2 13998 seqf1olem2 14015 bpolylem 15999 reeff1 16070 sscres 17777 fullsubc 17807 fullresc 17808 funcres2c 17861 dmaf 18009 cdaf 18010 frmdplusg 18777 frmdss2 18786 gass 19213 dprdfadd 19938 rngmgpf 20058 mgpf 20149 prdscrngd 20217 rnghmresfn 20511 rnghmsscmap2 20521 rnghmsscmap 20522 rhmresfn 20540 rhmsscmap2 20550 rhmsscmap 20551 subrgascl 21938 upxp 23447 uptx 23449 cnmpt1st 23492 cnmpt2nd 23493 cnextfres1 23892 prdstmdd 23948 ressprdsds 24197 prdsxmslem2 24358 xrsdsre 24646 itg1addlem4OLD 25549 recosf1o 26384 resinf1o 26385 mpodvdsmulf1o 27040 dvdsmulf1o 27042 ex-fpar 30149 sspg 30415 ssps 30417 sspmlem 30419 sspn 30423 hhssnv 30951 ressupprn 32346 1stpreimas 32361 cnre2csqlem 33355 raddcn 33374 carsggect 33782 subiwrdlen 33850 signsvtn0 34046 signstres 34051 bnj1253 34493 bnj1280 34496 subfacp1lem5 34640 cvmlift2lem9a 34759 filnetlem4 35732 finixpnum 36939 poimirlem4 36958 poimirlem8 36962 ftc1anclem3 37029 isdrngo2 37292 diaintclN 40395 dibintclN 40504 dihintcl 40681 imaiinfv 41896 fnwe2lem2 42258 aomclem6 42266 deg1mhm 42414 limsupvaluz2 44915 supcnvlimsup 44917 limsupgtlem 44954 resincncf 45052 icccncfext 45064 dvnprodlem1 45123 fourierdlem42 45326 fourierdlem73 45356 fdivmpt 47390 |
Copyright terms: Public domain | W3C validator |