MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnssres Structured version   Visualization version   GIF version

Theorem fnssres 5904
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fnssres ((𝐹 Fn 𝐴𝐵𝐴) → (𝐹𝐵) Fn 𝐵)

Proof of Theorem fnssres
StepHypRef Expression
1 fnssresb 5903 . 2 (𝐹 Fn 𝐴 → ((𝐹𝐵) Fn 𝐵𝐵𝐴))
21biimpar 500 1 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐹𝐵) Fn 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wss 3539  cres 5030   Fn wfn 5785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-res 5040  df-fun 5792  df-fn 5793
This theorem is referenced by:  fnresin1  5905  fnresin2  5906  fssres  5968  fvreseq0  6210  fnreseql  6220  ffvresb  6286  fnressn  6308  soisores  6455  ofres  6788  fnsuppres  7186  tfrlem1  7336  tz7.48lem  7400  tz7.49c  7405  resixp  7806  ixpfi2  8124  dfac12lem1  8825  ackbij2lem3  8923  cfsmolem  8952  alephsing  8958  ttukeylem3  9193  iunfo  9217  fpwwe2lem8  9315  mulnzcnopr  10522  seqfeq2  12641  seqf1olem2  12658  swrd0len  13220  swrdccat1  13255  bpolylem  14564  reeff1  14635  eucalg  15084  sscres  16252  fullsubc  16279  fullresc  16280  funcres2c  16330  dmaf  16468  cdaf  16469  frmdplusg  17160  frmdss2  17169  gass  17503  dprdfadd  18188  mgpf  18328  prdscrngd  18382  subrgascl  19265  mdetrsca  20170  upxp  21178  uptx  21180  cnmpt1st  21223  cnmpt2nd  21224  cnextfres1  21624  prdstmdd  21679  ressprdsds  21927  prdsxmslem2  22085  xrsdsre  22353  itg1addlem4  23189  recosf1o  24002  resinf1o  24003  dvdsmulf1o  24637  eupath2lem3  26272  sspg  26771  ssps  26773  sspmlem  26775  sspn  26779  hhssnv  27311  1stpreimas  28672  cnre2csqlem  29090  rmulccn  29108  raddcn  29109  carsggect  29513  subiwrdlen  29581  signsvtn0  29779  signstres  29784  bnj1253  30145  bnj1280  30148  subfacp1lem3  30224  subfacp1lem5  30226  cvmlift2lem9a  30345  nodenselem6  30891  filnetlem4  31352  finixpnum  32360  poimirlem4  32379  poimirlem8  32383  ftc1anclem3  32453  isdrngo2  32723  diaintclN  35161  dibintclN  35270  dihintcl  35447  imaiinfv  36070  fnwe2lem2  36435  aomclem6  36443  deg1mhm  36600  resincncf  38557  icccncfext  38570  dvnprodlem1  38633  fourierdlem42  38839  fourierdlem73  38869  pfxccat1  40071  1wlkres  40874  rnghmresfn  41750  rnghmsscmap2  41760  rnghmsscmap  41761  rhmresfn  41796  rhmsscmap2  41806  rhmsscmap  41807  fdivmpt  42127
  Copyright terms: Public domain W3C validator