![]() |
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 6237 | . 2 ⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) | |
2 | 1 | biimpar 471 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ⊆ wss 3799 ↾ cres 5345 Fn wfn 6119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4875 df-opab 4937 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-res 5355 df-fun 6126 df-fn 6127 |
This theorem is referenced by: fnresin1 6239 fnresin2 6240 fssres 6308 fvreseq0 6567 fnreseql 6577 ffvresb 6644 fnressn 6677 soisores 6833 oprres 7063 ofres 7174 fnsuppres 7588 tfrlem1 7739 tz7.48lem 7803 tz7.49c 7808 resixp 8211 ixpfi2 8534 dfac12lem1 9281 ackbij2lem3 9379 cfsmolem 9408 alephsing 9414 ttukeylem3 9649 iunfo 9677 fpwwe2lem8 9775 mulnzcnopr 10999 seqfeq2 13119 seqf1olem2 13136 swrd0lenOLD 13709 swrdccat1OLD 13748 pfxccat1 13782 bpolylem 15152 reeff1 15223 sscres 16836 fullsubc 16863 fullresc 16864 funcres2c 16914 dmaf 17052 cdaf 17053 frmdplusg 17746 frmdss2 17755 gass 18085 dprdfadd 18774 mgpf 18914 prdscrngd 18968 subrgascl 19859 mdetrsca 20778 upxp 21798 uptx 21800 cnmpt1st 21843 cnmpt2nd 21844 cnextfres1 22243 prdstmdd 22298 ressprdsds 22547 prdsxmslem2 22705 xrsdsre 22984 itg1addlem4 23866 recosf1o 24682 resinf1o 24683 dvdsmulf1o 25334 wlkresOLD 26972 sspg 28139 ssps 28141 sspmlem 28143 sspn 28147 hhssnv 28677 1stpreimas 30032 cnre2csqlem 30502 rmulccn 30520 raddcn 30521 carsggect 30926 subiwrdlen 30994 signsvtn0 31195 signsvtn0OLD 31196 signstres 31201 bnj1253 31632 bnj1280 31635 subfacp1lem3 31711 subfacp1lem5 31713 cvmlift2lem9a 31832 filnetlem4 32915 finixpnum 33938 poimirlem4 33958 poimirlem8 33962 ftc1anclem3 34031 isdrngo2 34300 diaintclN 37134 dibintclN 37243 dihintcl 37420 imaiinfv 38101 fnwe2lem2 38465 aomclem6 38473 deg1mhm 38629 fnssresd 40283 limsupvaluz2 40766 supcnvlimsup 40768 limsupgtlem 40805 resincncf 40884 icccncfext 40896 dvnprodlem1 40957 fourierdlem42 41161 fourierdlem73 41191 rnghmresfn 42811 rnghmsscmap2 42821 rnghmsscmap 42822 rhmresfn 42857 rhmsscmap2 42867 rhmsscmap 42868 fdivmpt 43182 |
Copyright terms: Public domain | W3C validator |