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

Definition df-f 5487
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5910, dff3 5911, and dff4 5912. (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 5479 . 2  wff  F : A
--> B
53, 1wfn 5478 . . 3  wff  F  Fn  A
63crn 4908 . . . 4  class  ran  F
76, 2wss 3306 . . 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  5605  feq2  5606  feq3  5607  nff  5618  ffn  5620  dffn2  5621  frn  5626  dffn3  5627  fss  5628  fco  5629  funssxp  5633  fun  5636  fnfco  5638  fssres  5639  fcoi2  5647  fint  5651  fin  5652  f0  5656  fconst  5658  f1ssr  5674  fof  5682  dff1o2  5708  fun11iun  5724  ffoss  5736  dff2  5910  dff3  5911  fmpt  5919  ffnfv  5923  ffvresb  5929  fpr  5943  idref  6008  dff1o6  6042  fliftf  6066  1stcof  6403  2ndcof  6404  smores  6643  smores2  6645  iordsmo  6648  map0e  7080  sbthlem9  7254  sucdom2  7332  inf3lem6  7617  alephsmo  8014  alephsing  8187  axdc3lem2  8362  smobeth  8492  fpwwe2lem11  8546  gch3  8582  gruiun  8705  gruima  8708  nqerf  8838  om2uzf1oi  11324  fclim  12378  invf  14024  funcres2b  14125  funcres2c  14129  hofcllem  14386  hofcl  14387  resmhm2b  14792  gsumval2  14814  frmdss2  14839  gsumval3a  15543  subgdmdprd  15623  cnrest  17380  cnrest2  17381  lmss  17393  concn  17520  txflf  18069  cnextf  18128  clsnsg  18170  tgpconcomp  18173  psmetxrge0  18375  causs  19282  ellimc2  19795  perfdvf  19821  c1lip2  19913  dvne0  19926  plyeq0  20161  plyreres  20231  aannenlem1  20276  taylf  20308  ulmss  20344  ausisusgra  21411  usgraedgrnv  21428  usgraexmpl  21451  cusgrarn  21499  hhssnv  22795  pjfi  23237  fdmrn  24070  measdivcstOLD  24609  sitgf  24691  cvmlift2lem9a  25021  elno2  25640  elno3  25641  nodenselem6  25672  mptelee  25865  isbnd3  26531  lsslindf  27315  indlcim  27325  dvsid  27563  stoweidlem27  27790  stoweidlem29  27792  stoweidlem31  27794  ffnafv  28049  sbcf  28115  uhgraedgrnv  28350  dihf11lem  32162
  Copyright terms: Public domain W3C validator