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

Theorem fnssres 5699
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fnssres

Proof of Theorem fnssres
StepHypRef Expression
1 fnssresb 5698 . 2
21biimpar 485 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  C_wss 3475  |`cres 5006  Fnwfn 5588
This theorem is referenced by:  fnresin1  5700  fnresin2  5701  fssres  5756  fvreseq0  5987  fnreseql  5997  ffvresb  6062  fnressn  6083  fnsuppresOLD  6131  soisores  6223  ofres  6555  fnsuppres  6946  tfrlem1  7064  tz7.48lem  7125  tz7.49c  7130  resixp  7524  ixpfi2  7838  dfac12lem1  8544  ackbij2lem3  8642  cfsmolem  8671  alephsing  8677  ttukeylem3  8912  iunfo  8935  fpwwe2lem8  9036  mulnzcnopr  10220  seqfeq2  12130  seqf1olem2  12147  swrd0len  12649  swrdccat1  12682  reeff1  13855  eucalg  14216  sscres  15192  fullsubc  15219  fullresc  15220  funcres2c  15270  dmaf  15376  cdaf  15377  frmdplusg  16022  frmdss2  16031  gass  16339  dprdfadd  17060  dprdfaddOLD  17067  mgpf  17210  prdscrngd  17262  subrgascl  18163  mdetrsca  19105  upxp  20124  uptx  20126  cnmpt1st  20169  cnmpt2nd  20170  cnextfres  20568  prdstmdd  20622  ressprdsds  20874  prdsxmslem2  21032  xrsdsre  21315  itg1addlem4  22106  recosf1o  22922  resinf1o  22923  dvdsmulf1o  23470  eupath2lem3  24979  ghgrpOLD  25370  sspg  25641  ssps  25643  sspmlem  25645  sspn  25649  hhssnv  26180  cnre2csqlem  27892  rmulccn  27910  raddcn  27911  subiwrdlen  28325  signsvtn0  28527  signstres  28532  subfacp1lem3  28626  subfacp1lem5  28628  cvmlift2lem9a  28748  nodenselem6  29446  bpolylem  29810  finixpnum  30038  ftc1anclem3  30092  filnetlem4  30199  isdrngo2  30361  imaiinfv  30625  fnwe2lem2  30997  aomclem6  31005  deg1mhm  31167  resincncf  31677  icccncfext  31690  dvnprodlem1  31743  fourierdlem42  31931  fourierdlem73  31962  rnghmresfn  32771  rnghmsscmap2  32781  rnghmsscmap  32782  rhmresfn  32817  rhmsscmap2  32827  rhmsscmap  32828  bnj1253  34073  bnj1280  34076  diaintclN  36785  dibintclN  36894  dihintcl  37071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-res 5016  df-fun 5595  df-fn 5596
  Copyright terms: Public domain W3C validator