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

Definition df-f 5605
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 6049, dff3 6050, and dff4 6051. (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 5597 . 2  wff  F : A
--> B
53, 1wfn 5596 . . 3  wff  F  Fn  A
63crn 4855 . . . 4  class  ran  F
76, 2wss 3442 . . 3  wff  ran  F  C_  B
85, 7wa 370 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 187 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  feq1  5728  feq2  5729  feq3  5730  nff  5742  sbcfg  5744  ffn  5746  dffn2  5747  frn  5752  dffn3  5753  fss  5754  fco  5756  funssxp  5759  fdmrn  5761  fun  5763  fnfco  5765  fssres  5766  fcoi2  5775  fint  5779  fin  5780  f0  5781  fconst  5786  f1ssr  5802  fof  5810  dff1o2  5836  dff2  6049  dff3  6050  fmpt  6058  ffnfv  6064  ffvresb  6069  fpr  6087  idref  6161  dff1o6  6189  fliftf  6223  fun11iun  6767  ffoss  6768  1stcof  6835  2ndcof  6836  smores  7079  smores2  7081  iordsmo  7084  sbthlem9  7696  sucdom2  7774  inf3lem6  8138  alephsmo  8531  alephsing  8704  axdc3lem2  8879  smobeth  9009  fpwwe2lem11  9064  gch3  9100  gruiun  9223  gruima  9226  nqerf  9354  om2uzf1oi  12164  fclim  13595  invf  15624  funcres2b  15753  funcres2c  15757  hofcllem  16094  hofcl  16095  gsumval2  16474  resmhm2b  16559  frmdss2  16598  gsumval3a  17472  subgdmdprd  17602  lsslindf  19319  indlcim  19329  cnrest2  20233  lmss  20245  concn  20372  txflf  20952  cnextf  21012  clsnsg  21055  tgpconcomp  21058  psmetxrge0  21260  causs  22161  ellimc2  22709  perfdvf  22735  c1lip2  22827  dvne0  22840  plyeq0  23033  plyreres  23104  aannenlem1  23149  taylf  23181  ulmss  23217  mptelee  24771  ausisusgra  24928  usgraedgrnv  24950  usgraexmpl  24974  cusgrarn  25032  hhssnv  26750  pjfi  27192  maprnin  28159  measdivcstOLD  28885  sitgf  29008  eulerpartlemn  29040  cvmlift2lem9a  29814  elno2  30328  elno3  30329  nodenselem6  30360  icoreresf  31489  poimirlem30  31673  poimirlem31  31674  isbnd3  31819  dihf11lem  34542  dvsid  36316  stoweidlem27  37455  stoweidlem29  37457  stoweidlem29OLD  37458  stoweidlem31  37460  fourierdlem15  37552  ffnafv  38062  iccpartf  38134  uhgraedgrnv  38418  resmgmhm2b  38557
  Copyright terms: Public domain W3C validator