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 4854 . . . 4  class  ran  F
76, 2wss 3436 . . 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  7082  smores2  7084  iordsmo  7087  sbthlem9  7699  sucdom2  7777  inf3lem6  8147  alephsmo  8540  alephsing  8713  axdc3lem2  8888  smobeth  9018  fpwwe2lem11  9072  gch3  9108  gruiun  9231  gruima  9234  nqerf  9362  om2uzf1oi  12173  fclim  13616  invf  15672  funcres2b  15801  funcres2c  15805  hofcllem  16142  hofcl  16143  gsumval2  16522  resmhm2b  16607  frmdss2  16646  gsumval3a  17536  subgdmdprd  17666  lsslindf  19386  indlcim  19396  cnrest2  20300  lmss  20312  concn  20439  txflf  21019  cnextf  21079  clsnsg  21122  tgpconcomp  21125  psmetxrge0  21327  causs  22266  ellimc2  22830  perfdvf  22856  c1lip2  22948  dvne0  22961  plyeq0  23163  plyreres  23234  aannenlem1  23282  taylf  23314  ulmss  23350  mptelee  24923  ausisusgra  25080  usgraedgrnv  25102  usgraexmplef  25126  cusgrarn  25185  hhssnv  26913  pjfi  27355  maprnin  28322  measdivcstOLD  29054  sitgf  29188  eulerpartlemn  29222  cvmlift2lem9a  30034  elno2  30548  elno3  30549  nodenselem6  30580  icoreresf  31719  poimirlem30  31934  poimirlem31  31935  isbnd3  32080  dihf11lem  34803  dvsid  36650  stoweidlem27  37827  stoweidlem29  37829  stoweidlem29OLD  37830  stoweidlem31  37832  fourierdlem15  37924  ffnafv  38543  iccpartf  38615  ausgrusgrb  39047  ausgrumgri  39049  subuhgr  39131  subumgr  39132  subusgr  39133  uhgraedgrnv  39283  resmgmhm2b  39420
  Copyright terms: Public domain W3C validator