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

Definition df-fn 5596
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5737, dffn3 5743, dffn4 5806, and dffn5 5918. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fn

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wfn 5588 . 2
41wfun 5587 . . 3
51cdm 5004 . . . 4
65, 2wceq 1395 . . 3
74, 6wa 369 . 2
83, 7wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  funfn  5622  fnsng  5640  fnprg  5647  fntpg  5648  fntp  5649  fncnv  5657  fneq1  5674  fneq2  5675  nffn  5682  fnfun  5683  fndm  5685  fnun  5692  fnco  5694  fnssresb  5698  fnres  5702  fnresi  5703  fn0  5705  fnopabg  5709  sbcfng  5733  fdmrn  5751  fcoi1  5764  f00  5772  f1cnvcnv  5794  fores  5809  dff1o4  5829  foimacnv  5838  funfv  5940  fvimacnvALT  6006  respreima  6016  dff3  6044  fpr  6079  fnsnb  6090  fnprb  6129  fnprOLD  6130  fnex  6139  fliftf  6213  fnoprabg  6403  fun11iun  6760  f1oweALT  6784  curry1  6892  curry2  6895  tposfn2  6996  tfrlem10  7075  tfr1  7085  frfnom  7119  undifixp  7525  sbthlem9  7655  fodomr  7688  rankf  8233  cardf2  8345  axdc3lem2  8852  nqerf  9329  axaddf  9543  axmulf  9544  uzrdgfni  12069  hashkf  12407  shftfn  12906  imasaddfnlem  14925  imasvscafn  14934  cnextf  20566  ftc1cn  22444  grporn  25214  mptfnf  27499  ffsrn  27552  measdivcstOLD  28195  wfrlem13  29355  wfr1  29359  nofnbday  29412  elno2  29414  bdayfn  29439  fnsingle  29569  fnimage  29579  imageval  29580  dfrdg4  29600  tfrqfree  29601  ftc1cnnc  30089  fnresfnco  32211  funcoressn  32212  afvco2  32261  bnj145OLD  33782  bnj1422  33896
  Copyright terms: Public domain W3C validator