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

Definition df-f 4604
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5524, dff3 5525, and dff4 5526. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wf 4588 . 2  wff  F : A
--> B
53, 1wfn 4587 . . 3  wff  F  Fn  A
63crn 4581 . . . 4  class  ran  F
76, 2wss 3078 . . 3  wff  ran  F  C_  B
85, 7wa 360 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 178 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5232  feq2  5233  feq3  5234  nff  5244  ffn  5246  dffn2  5247  frn  5252  dffn3  5253  fss  5254  fco  5255  funssxp  5259  fun  5262  fnfco  5264  fssres  5265  fcoi2  5273  fint  5277  fin  5278  f0  5282  fconst  5284  f1ssr  5300  fof  5308  dff1o2  5334  fun11iun  5350  ffoss  5362  dff2  5524  dff3  5525  fmpt  5533  ffnfv  5537  ffvresb  5542  fpr  5556  idref  5611  dff1o6  5643  fliftf  5666  1stcof  5999  2ndcof  6000  smores  6255  smores2  6257  iordsmo  6260  map0e  6691  sbthlem9  6864  sucdom2  6942  inf3lem6  7218  alephsmo  7613  alephsing  7786  axdc3lem2  7961  smobeth  8088  fpwwe2lem11  8142  gch3  8182  gruiun  8301  gruima  8304  nqerf  8434  om2uzf1oi  10894  fclim  11904  invf  13514  funcres2b  13615  funcres2c  13619  hofcllem  13876  hofcl  13877  resmhm2b  14273  gsumval2  14295  frmdss2  14320  gsumval3a  15024  subgdmdprd  15104  cnrest  16845  cnrest2  16846  lmss  16858  concn  16984  txflf  17533  clsnsg  17624  tgpconcomp  17627  causs  18556  ellimc2  19059  perfdvf  19085  c1lip2  19177  dvne0  19190  plyeq0  19425  plyreres  19495  aannenlem1  19540  taylf  19572  ulmss  19606  hhssnv  21671  pjfi  22131  cvmlift2lem9a  23005  elno2  23475  elno3  23476  axdenselem6  23508  mptelee  23697  domrancur1b  24366  trnij  24781  fnckleb  25212  isbnd3  25674  lsslindf  26466  indlcim  26476  dvsid  26714  dihf11lem  30215
  Copyright terms: Public domain W3C validator