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

Theorem fnssres 5704
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fnssres  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( F  |`  B )  Fn  B )

Proof of Theorem fnssres
StepHypRef Expression
1 fnssresb 5703 . 2  |-  ( F  Fn  A  ->  (
( F  |`  B )  Fn  B  <->  B  C_  A
) )
21biimpar 487 1  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( F  |`  B )  Fn  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    C_ wss 3436    |` cres 4852    Fn wfn 5593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-res 4862  df-fun 5600  df-fn 5601
This theorem is referenced by:  fnresin1  5705  fnresin2  5706  fssres  5763  fvreseq0  5994  fnreseql  6004  ffvresb  6066  fnressn  6088  soisores  6230  ofres  6558  fnsuppres  6950  tfrlem1  7099  tz7.48lem  7163  tz7.49c  7168  resixp  7562  ixpfi2  7875  dfac12lem1  8574  ackbij2lem3  8672  cfsmolem  8701  alephsing  8707  ttukeylem3  8942  iunfo  8965  fpwwe2lem8  9063  mulnzcnopr  10259  seqfeq2  12236  seqf1olem2  12253  swrd0len  12769  swrdccat1  12804  bpolylem  14089  reeff1  14162  eucalg  14534  sscres  15716  fullsubc  15743  fullresc  15744  funcres2c  15794  dmaf  15932  cdaf  15933  frmdplusg  16626  frmdss2  16635  gass  16943  dprdfadd  17641  mgpf  17780  prdscrngd  17829  subrgascl  18709  mdetrsca  19615  upxp  20625  uptx  20627  cnmpt1st  20670  cnmpt2nd  20671  cnextfres1  21070  prdstmdd  21125  ressprdsds  21373  prdsxmslem2  21531  xrsdsre  21815  itg1addlem4  22644  recosf1o  23471  resinf1o  23472  dvdsmulf1o  24110  eupath2lem3  25693  ghgrpOLD  26082  sspg  26353  ssps  26355  sspmlem  26357  sspn  26361  hhssnv  26901  1stpreimas  28276  cnre2csqlem  28712  rmulccn  28730  raddcn  28731  carsggect  29146  subiwrdlen  29215  signsvtn0  29455  signstres  29460  bnj1253  29822  bnj1280  29825  subfacp1lem3  29901  subfacp1lem5  29903  cvmlift2lem9a  30022  nodenselem6  30568  filnetlem4  31030  finixpnum  31844  poimirlem4  31858  poimirlem8  31862  ftc1anclem3  31933  isdrngo2  32111  diaintclN  34545  dibintclN  34654  dihintcl  34831  imaiinfv  35454  fnwe2lem2  35829  aomclem6  35837  deg1mhm  36004  resincncf  37572  icccncfext  37585  dvnprodlem1  37641  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem73  37863  pfxccat1  38663  rnghmresfn  39237  rnghmsscmap2  39247  rnghmsscmap  39248  rhmresfn  39283  rhmsscmap2  39293  rhmsscmap  39294  fdivmpt  39625
  Copyright terms: Public domain W3C validator