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

Definition df-f 5226
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5634, dff3 5635, and dff4 5636. (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 5218 . 2  wff  F : A
--> B
53, 1wfn 5217 . . 3  wff  F  Fn  A
63crn 4690 . . . 4  class  ran  F
76, 2wss 3154 . . 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  5341  feq2  5342  feq3  5343  nff  5353  ffn  5355  dffn2  5356  frn  5361  dffn3  5362  fss  5363  fco  5364  funssxp  5368  fun  5371  fnfco  5373  fssres  5374  fcoi2  5382  fint  5386  fin  5387  f0  5391  fconst  5393  f1ssr  5409  fof  5417  dff1o2  5443  fun11iun  5459  ffoss  5471  dff2  5634  dff3  5635  fmpt  5643  ffnfv  5647  ffvresb  5652  fpr  5666  idref  5721  dff1o6  5753  fliftf  5776  1stcof  6109  2ndcof  6110  smores  6365  smores2  6367  iordsmo  6370  map0e  6801  sbthlem9  6975  sucdom2  7053  inf3lem6  7330  alephsmo  7725  alephsing  7898  axdc3lem2  8073  smobeth  8204  fpwwe2lem11  8258  gch3  8298  gruiun  8417  gruima  8420  nqerf  8550  om2uzf1oi  11011  fclim  12022  invf  13665  funcres2b  13766  funcres2c  13770  hofcllem  14027  hofcl  14028  resmhm2b  14433  gsumval2  14455  frmdss2  14480  gsumval3a  15184  subgdmdprd  15264  cnrest  17008  cnrest2  17009  lmss  17021  concn  17147  txflf  17696  clsnsg  17787  tgpconcomp  17790  causs  18719  ellimc2  19222  perfdvf  19248  c1lip2  19340  dvne0  19353  plyeq0  19588  plyreres  19658  aannenlem1  19703  taylf  19735  ulmss  19769  hhssnv  21834  pjfi  22276  fdmrn  23029  cvmlift2lem9a  23239  elno2  23709  elno3  23710  axdenselem6  23742  mptelee  23931  domrancur1b  24600  trnij  25015  fnckleb  25446  isbnd3  25908  lsslindf  26700  indlcim  26710  dvsid  26948  fnvinran  27085  cncmpmax  27103  stoweidlem27  27176  stoweidlem29  27178  stoweidlem31  27180  ffnafv  27413  dihf11lem  30724
  Copyright terms: Public domain W3C validator