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 6462 | . 2 ⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) | |
2 | 1 | biimpar 480 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ⊆ wss 3934 ↾ cres 5550 Fn wfn 6343 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5058 df-opab 5120 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-res 5560 df-fun 6350 df-fn 6351 |
This theorem is referenced by: fnssresd 6464 fnresin1 6465 fnresin2 6466 fnresi 6469 fssres 6537 fvreseq0 6801 fnreseql 6811 ffvresb 6881 fnressn 6913 soisores 7072 oprres 7308 ofres 7417 fsplitfpar 7806 fnsuppres 7849 tfrlem1 8004 tz7.48lem 8069 tz7.49c 8074 resixp 8489 ixpfi2 8814 dfac12lem1 9561 ackbij2lem3 9655 cfsmolem 9684 alephsing 9690 ttukeylem3 9925 iunfo 9953 fpwwe2lem8 10051 mulnzcnopr 11278 seqfeq2 13385 seqf1olem2 13402 bpolylem 15394 reeff1 15465 sscres 17085 fullsubc 17112 fullresc 17113 funcres2c 17163 dmaf 17301 cdaf 17302 frmdplusg 18011 frmdss2 18020 gass 18423 dprdfadd 19134 mgpf 19301 prdscrngd 19355 subrgascl 20270 mdetrsca 21204 upxp 22223 uptx 22225 cnmpt1st 22268 cnmpt2nd 22269 cnextfres1 22668 prdstmdd 22724 ressprdsds 22973 prdsxmslem2 23131 xrsdsre 23410 itg1addlem4 24292 recosf1o 25111 resinf1o 25112 dvdsmulf1o 25763 ex-fpar 28233 sspg 28497 ssps 28499 sspmlem 28501 sspn 28505 hhssnv 29033 1stpreimas 30433 dimkerim 31016 cnre2csqlem 31146 rmulccn 31164 raddcn 31165 carsggect 31569 subiwrdlen 31637 signsvtn0 31833 signstres 31838 bnj1253 32282 bnj1280 32285 subfacp1lem3 32422 subfacp1lem5 32424 cvmlift2lem9a 32543 filnetlem4 33722 finixpnum 34869 poimirlem4 34888 poimirlem8 34892 ftc1anclem3 34961 isdrngo2 35228 diaintclN 38186 dibintclN 38295 dihintcl 38472 imaiinfv 39281 fnwe2lem2 39642 aomclem6 39650 deg1mhm 39798 limsupvaluz2 42009 supcnvlimsup 42011 limsupgtlem 42048 resincncf 42148 icccncfext 42160 dvnprodlem1 42221 fourierdlem42 42425 fourierdlem73 42455 rnghmresfn 44225 rnghmsscmap2 44235 rnghmsscmap 44236 rhmresfn 44271 rhmsscmap2 44281 rhmsscmap 44282 fdivmpt 44591 |
Copyright terms: Public domain | W3C validator |