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

Definition df-f 5450
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5873, dff3 5874, and dff4 5875. (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 5442 . 2  wff  F : A
--> B
53, 1wfn 5441 . . 3  wff  F  Fn  A
63crn 4871 . . . 4  class  ran  F
76, 2wss 3312 . . 3  wff  ran  F  C_  B
85, 7wa 359 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 177 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5568  feq2  5569  feq3  5570  nff  5581  ffn  5583  dffn2  5584  frn  5589  dffn3  5590  fss  5591  fco  5592  funssxp  5596  fun  5599  fnfco  5601  fssres  5602  fcoi2  5610  fint  5614  fin  5615  f0  5619  fconst  5621  f1ssr  5637  fof  5645  dff1o2  5671  fun11iun  5687  ffoss  5699  dff2  5873  dff3  5874  fmpt  5882  ffnfv  5886  ffvresb  5892  fpr  5906  idref  5971  dff1o6  6005  fliftf  6029  1stcof  6366  2ndcof  6367  smores  6606  smores2  6608  iordsmo  6611  map0e  7043  sbthlem9  7217  sucdom2  7295  inf3lem6  7580  alephsmo  7975  alephsing  8148  axdc3lem2  8323  smobeth  8453  fpwwe2lem11  8507  gch3  8547  gruiun  8666  gruima  8669  nqerf  8799  om2uzf1oi  11285  fclim  12339  invf  13985  funcres2b  14086  funcres2c  14090  hofcllem  14347  hofcl  14348  resmhm2b  14753  gsumval2  14775  frmdss2  14800  gsumval3a  15504  subgdmdprd  15584  cnrest  17341  cnrest2  17342  lmss  17354  concn  17481  txflf  18030  cnextf  18089  clsnsg  18131  tgpconcomp  18134  psmetxrge0  18336  causs  19243  ellimc2  19756  perfdvf  19782  c1lip2  19874  dvne0  19887  plyeq0  20122  plyreres  20192  aannenlem1  20237  taylf  20269  ulmss  20305  ausisusgra  21372  usgraedgrnv  21389  usgraexmpl  21412  cusgrarn  21460  hhssnv  22756  pjfi  23198  fdmrn  24031  measdivcstOLD  24570  sitgf  24652  cvmlift2lem9a  24982  elno2  25601  elno3  25602  nodenselem6  25633  mptelee  25826  isbnd3  26484  lsslindf  27268  indlcim  27278  dvsid  27516  stoweidlem27  27743  stoweidlem29  27745  stoweidlem31  27747  ffnafv  28002  uhgraedgrnv  28255  dihf11lem  32001
  Copyright terms: Public domain W3C validator