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

Definition df-f 5275
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5688, dff3 5689, and dff4 5690. (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 5267 . 2  wff  F : A
--> B
53, 1wfn 5266 . . 3  wff  F  Fn  A
63crn 4706 . . . 4  class  ran  F
76, 2wss 3165 . . 3  wff  ran  F  C_  B
85, 7wa 358 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 176 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5391  feq2  5392  feq3  5393  nff  5403  ffn  5405  dffn2  5406  frn  5411  dffn3  5412  fss  5413  fco  5414  funssxp  5418  fun  5421  fnfco  5423  fssres  5424  fcoi2  5432  fint  5436  fin  5437  f0  5441  fconst  5443  f1ssr  5459  fof  5467  dff1o2  5493  fun11iun  5509  ffoss  5521  dff2  5688  dff3  5689  fmpt  5697  ffnfv  5701  ffvresb  5706  fpr  5720  idref  5775  dff1o6  5807  fliftf  5830  1stcof  6163  2ndcof  6164  smores  6385  smores2  6387  iordsmo  6390  map0e  6821  sbthlem9  6995  sucdom2  7073  inf3lem6  7350  alephsmo  7745  alephsing  7918  axdc3lem2  8093  smobeth  8224  fpwwe2lem11  8278  gch3  8318  gruiun  8437  gruima  8440  nqerf  8570  om2uzf1oi  11032  fclim  12043  invf  13686  funcres2b  13787  funcres2c  13791  hofcllem  14048  hofcl  14049  resmhm2b  14454  gsumval2  14476  frmdss2  14501  gsumval3a  15205  subgdmdprd  15285  cnrest  17029  cnrest2  17030  lmss  17042  concn  17168  txflf  17717  clsnsg  17808  tgpconcomp  17811  causs  18740  ellimc2  19243  perfdvf  19269  c1lip2  19361  dvne0  19374  plyeq0  19609  plyreres  19679  aannenlem1  19724  taylf  19756  ulmss  19790  hhssnv  21857  pjfi  22299  fdmrn  23051  measdivcstOLD  23566  measdivcst  23567  cvmlift2lem9a  23849  elno2  24379  elno3  24380  nodenselem6  24411  mptelee  24595  domrancur1b  25303  trnij  25718  fnckleb  26149  isbnd3  26611  lsslindf  27403  indlcim  27413  dvsid  27651  fnvinran  27788  cncmpmax  27806  stoweidlem27  27879  stoweidlem29  27881  stoweidlem31  27883  ffnafv  28139  usgraedgrnv  28257  usgraexmpl  28267  dihf11lem  32078
  Copyright terms: Public domain W3C validator