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

Theorem fnfun 5683
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnfun

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 5596 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  domcdm 5004  Funwfun 5587  Fnwfn 5588
This theorem is referenced by:  fnrel  5684  funfni  5686  fnco  5694  fnssresb  5698  ffun  5738  f1fun  5788  f1ofun  5823  fnbrfvb  5913  fvelimab  5929  fvun1  5944  elpreima  6007  respreima  6016  fnsnb  6090  fnprb  6129  fnprOLD  6130  fconst3  6135  fnfvima  6150  fnunirn  6165  nvof1o  6186  f1eqcocnv  6204  fnexALT  6766  curry1  6892  curry2  6895  suppvalfn  6925  suppfnss  6944  fnsuppres  6946  tfrlem4  7067  tfrlem5  7068  tfrlem11  7076  tz7.48-2  7126  tz7.49  7129  fndmeng  7612  fnfi  7818  fodomfi  7819  fczfsuppd  7867  marypha2lem4  7918  inf0  8059  noinfepOLD  8098  r1elss  8245  dfac8alem  8431  alephfp  8510  dfac3  8523  dfac9  8537  dfac12lem1  8544  dfac12lem2  8545  r1om  8645  cfsmolem  8671  alephsing  8677  zorn2lem1  8897  zorn2lem5  8901  zorn2lem6  8902  zorn2lem7  8903  ttukeylem3  8912  ttukeylem6  8915  smobeth  8982  fpwwe2lem9  9037  wunr1om  9118  tskr1om  9166  tskr1om2  9167  uzrdg0i  12070  uzrdgsuci  12071  hashkf  12407  shftfn  12906  phimullem  14309  imasaddvallem  14926  imasvscaval  14935  frmdss2  16031  dprdvalOLD  17036  lcomfsupp  17550  lidlval  17838  rspval  17839  psrbagev1  18177  psgnghm  18616  frlmsslsp  18829  frlmsslspOLD  18830  iscldtop  19596  2ndcomap  19959  qtoptop  20201  basqtop  20212  qtoprest  20218  kqfvima  20231  isr0  20238  kqreglem1  20242  kqnrmlem1  20244  kqnrmlem2  20245  elrnust  20727  ustbas  20730  uniiccdif  21987  eupap1  24976  fcoinver  27460  fnct  27536  fimaproj  27836  sseqf  28331  sseqfv2  28333  elorrvc  28402  wfrlem2  29344  wfrlem14  29356  frrlem2  29388  filnetlem4  30199  heibor1lem  30305  ismrc  30633  dnnumch1  30990  aomclem4  31003  aomclem6  31005  icccncfext  31690  stoweidlem29  31811  stoweidlem59  31841  fnresfnco  32211  funcoressn  32212  fnbrafvb  32239  tz6.12-afv  32258  afvco2  32261  resfnfinfin  32310  plusfreseq  32460  dfrngc2  32780  dfringc2  32826  rngcresringcat  32838  mndpsuppss  32964  mndpfsupp  32969  bnj142OLD  33781  bnj930  33828  bnj1371  34085  bnj1497  34116  diaf11N  36776  dibf11N  36888  dibclN  36889  dihintcl  37071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-fn 5596
  Copyright terms: Public domain W3C validator