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

Definition df-f 5460
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5883, dff3 5884, and dff4 5885. (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 5452 . 2  wff  F : A
--> B
53, 1wfn 5451 . . 3  wff  F  Fn  A
63crn 4881 . . . 4  class  ran  F
76, 2wss 3322 . . 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  5578  feq2  5579  feq3  5580  nff  5591  ffn  5593  dffn2  5594  frn  5599  dffn3  5600  fss  5601  fco  5602  funssxp  5606  fun  5609  fnfco  5611  fssres  5612  fcoi2  5620  fint  5624  fin  5625  f0  5629  fconst  5631  f1ssr  5647  fof  5655  dff1o2  5681  fun11iun  5697  ffoss  5709  dff2  5883  dff3  5884  fmpt  5892  ffnfv  5896  ffvresb  5902  fpr  5916  idref  5981  dff1o6  6015  fliftf  6039  1stcof  6376  2ndcof  6377  smores  6616  smores2  6618  iordsmo  6621  map0e  7053  sbthlem9  7227  sucdom2  7305  inf3lem6  7590  alephsmo  7985  alephsing  8158  axdc3lem2  8333  smobeth  8463  fpwwe2lem11  8517  gch3  8557  gruiun  8676  gruima  8679  nqerf  8809  om2uzf1oi  11295  fclim  12349  invf  13995  funcres2b  14096  funcres2c  14100  hofcllem  14357  hofcl  14358  resmhm2b  14763  gsumval2  14785  frmdss2  14810  gsumval3a  15514  subgdmdprd  15594  cnrest  17351  cnrest2  17352  lmss  17364  concn  17491  txflf  18040  cnextf  18099  clsnsg  18141  tgpconcomp  18144  psmetxrge0  18346  causs  19253  ellimc2  19766  perfdvf  19792  c1lip2  19884  dvne0  19897  plyeq0  20132  plyreres  20202  aannenlem1  20247  taylf  20279  ulmss  20315  ausisusgra  21382  usgraedgrnv  21399  usgraexmpl  21422  cusgrarn  21470  hhssnv  22766  pjfi  23208  fdmrn  24041  measdivcstOLD  24580  sitgf  24662  cvmlift2lem9a  24992  elno2  25611  elno3  25612  nodenselem6  25643  mptelee  25836  isbnd3  26495  lsslindf  27279  indlcim  27289  dvsid  27527  stoweidlem27  27754  stoweidlem29  27756  stoweidlem31  27758  ffnafv  28013  sbcf  28079  uhgraedgrnv  28314  dihf11lem  32126
  Copyright terms: Public domain W3C validator