Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fnssres | Structured version Visualization version Unicode version |
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fnssres |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnssresb 6003 | . 2 | |
2 | 1 | biimpar 502 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wss 3574 cres 5116 wfn 5883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-res 5126 df-fun 5890 df-fn 5891 |
This theorem is referenced by: fnresin1 6005 fnresin2 6006 fssres 6070 fvreseq0 6317 fnreseql 6327 ffvresb 6394 fnressn 6425 soisores 6577 oprres 6802 ofres 6913 fnsuppres 7322 tfrlem1 7472 tz7.48lem 7536 tz7.49c 7541 resixp 7943 ixpfi2 8264 dfac12lem1 8965 ackbij2lem3 9063 cfsmolem 9092 alephsing 9098 ttukeylem3 9333 iunfo 9361 fpwwe2lem8 9459 mulnzcnopr 10673 seqfeq2 12824 seqf1olem2 12841 swrd0len 13422 swrdccat1 13457 bpolylem 14779 reeff1 14850 eucalg 15300 sscres 16483 fullsubc 16510 fullresc 16511 funcres2c 16561 dmaf 16699 cdaf 16700 frmdplusg 17391 frmdss2 17400 gass 17734 dprdfadd 18419 mgpf 18559 prdscrngd 18613 subrgascl 19498 mdetrsca 20409 upxp 21426 uptx 21428 cnmpt1st 21471 cnmpt2nd 21472 cnextfres1 21872 prdstmdd 21927 ressprdsds 22176 prdsxmslem2 22334 xrsdsre 22613 itg1addlem4 23466 recosf1o 24281 resinf1o 24282 dvdsmulf1o 24920 wlkres 26567 sspg 27583 ssps 27585 sspmlem 27587 sspn 27591 hhssnv 28121 1stpreimas 29483 cnre2csqlem 29956 rmulccn 29974 raddcn 29975 carsggect 30380 subiwrdlen 30448 signsvtn0 30647 signstres 30652 bnj1253 31085 bnj1280 31088 subfacp1lem3 31164 subfacp1lem5 31166 cvmlift2lem9a 31285 filnetlem4 32376 finixpnum 33394 poimirlem4 33413 poimirlem8 33417 ftc1anclem3 33487 isdrngo2 33757 diaintclN 36347 dibintclN 36456 dihintcl 36633 imaiinfv 37256 fnwe2lem2 37621 aomclem6 37629 deg1mhm 37785 fnssresd 39482 limsupvaluz2 39970 supcnvlimsup 39972 limsupgtlem 40009 resincncf 40088 icccncfext 40100 dvnprodlem1 40161 fourierdlem42 40366 fourierdlem73 40396 pfxccat1 41410 rnghmresfn 41963 rnghmsscmap2 41973 rnghmsscmap 41974 rhmresfn 42009 rhmsscmap2 42019 rhmsscmap 42020 fdivmpt 42334 |
Copyright terms: Public domain | W3C validator |