| 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 6647 | . 2 ⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) | |
| 2 | 1 | biimpar 482 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 ⊆ wss 3907 ↾ cres 5653 Fn wfn 6520 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5250 ax-pr 5394 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-res 5663 df-fun 6527 df-fn 6528 |
| This theorem is referenced by: fnssresd 6649 fnresin1 6650 fnresin2 6651 fnresi 6654 fssres 6734 fvreseq0 7023 fnreseql 7033 ffvresb 7111 fnressn 7145 soisores 7315 oprres 7568 ofres 7683 fsplitfpar 8101 fnsuppres 8175 tfrlem1 8350 tz7.48lem 8416 tz7.49c 8421 resixp 8919 ixpfi2 9295 ttrclss 9677 dfac12lem1 10115 ackbij2lem3 10211 cfsmolem 10242 alephsing 10248 ttukeylem3 10483 iunfo 10511 fpwwe2lem7 10610 mulnzcnf 11848 seqfeq2 14049 seqf1olem2 14066 bpolylem 16090 reeff1 16164 sscres 17868 fullsubc 17895 fullresc 17896 funcres2c 17948 dmaf 18094 cdaf 18095 frmdplusg 18901 frmdss2 18910 gass 19359 dprdfadd 20080 rngmgpf 20223 mgpf 20318 prdscrngd 20391 rnghmresfn 20692 rnghmsscmap2 20702 rnghmsscmap 20703 rhmresfn 20721 rhmsscmap2 20731 rhmsscmap 20732 subrgascl 22174 upxp 23737 uptx 23739 cnmpt1st 23782 cnmpt2nd 23783 cnextfres1 24182 prdstmdd 24238 ressprdsds 24485 prdsxmslem2 24643 xrsdsre 24925 recosf1o 26654 resinf1o 26655 mpodvdsmulf1o 27312 dvdsmulf1o 27314 ex-fpar 30718 sspg 30985 ssps 30987 sspmlem 30989 sspn 30993 hhssnv 31521 ressupprn 32943 1stpreimas 32959 cnre2csqlem 34212 raddcn 34231 carsggect 34620 subiwrdlen 34688 signsvtn0 34869 signstres 34874 bnj1253 35317 bnj1280 35320 gblacfnacd 35452 subfacp1lem5 35542 cvmlift2lem9a 35661 filnetlem4 36749 finixpnum 38111 poimirlem4 38130 poimirlem8 38134 ftc1anclem3 38201 isdrngo2 38464 diaintclN 41689 dibintclN 41798 dihintcl 41975 imaiinfv 43281 fnwe2lem2 43635 aomclem6 43643 deg1mhm 43784 limsupvaluz2 46311 supcnvlimsup 46313 limsupgtlem 46350 resincncf 46448 icccncfext 46460 fourierdlem42 46722 fourierdlem73 46752 fdivmpt 49172 slotresfo 49529 basresposfo 49608 oppff1 49778 |
| Copyright terms: Public domain | W3C validator |