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

Definition df-f 4685
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5606, dff3 5607, and dff4 5608. (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 4669 . 2  wff  F : A
--> B
53, 1wfn 4668 . . 3  wff  F  Fn  A
63crn 4662 . . . 4  class  ran  F
76, 2wss 3127 . . 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  5313  feq2  5314  feq3  5315  nff  5325  ffn  5327  dffn2  5328  frn  5333  dffn3  5334  fss  5335  fco  5336  funssxp  5340  fun  5343  fnfco  5345  fssres  5346  fcoi2  5354  fint  5358  fin  5359  f0  5363  fconst  5365  f1ssr  5381  fof  5389  dff1o2  5415  fun11iun  5431  ffoss  5443  dff2  5606  dff3  5607  fmpt  5615  ffnfv  5619  ffvresb  5624  fpr  5638  idref  5693  dff1o6  5725  fliftf  5748  1stcof  6081  2ndcof  6082  smores  6337  smores2  6339  iordsmo  6342  map0e  6773  sbthlem9  6947  sucdom2  7025  inf3lem6  7302  alephsmo  7697  alephsing  7870  axdc3lem2  8045  smobeth  8176  fpwwe2lem11  8230  gch3  8270  gruiun  8389  gruima  8392  nqerf  8522  om2uzf1oi  10982  fclim  11992  invf  13632  funcres2b  13733  funcres2c  13737  hofcllem  13994  hofcl  13995  resmhm2b  14400  gsumval2  14422  frmdss2  14447  gsumval3a  15151  subgdmdprd  15231  cnrest  16975  cnrest2  16976  lmss  16988  concn  17114  txflf  17663  clsnsg  17754  tgpconcomp  17757  causs  18686  ellimc2  19189  perfdvf  19215  c1lip2  19307  dvne0  19320  plyeq0  19555  plyreres  19625  aannenlem1  19670  taylf  19702  ulmss  19736  hhssnv  21801  pjfi  22243  fdmrn  22996  cvmlift2lem9a  23206  elno2  23676  elno3  23677  axdenselem6  23709  mptelee  23898  domrancur1b  24567  trnij  24982  fnckleb  25413  isbnd3  25875  lsslindf  26667  indlcim  26677  dvsid  26915  fnvinran  27053  cncmpmax  27071  stoweidlem27  27111  stoweidlem29  27113  stoweidlem31  27115  dihf11lem  30623
  Copyright terms: Public domain W3C validator