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

Definition df-f 4650
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5571, dff3 5572, and dff4 5573. (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 4634 . 2  wff  F : A
--> B
53, 1wfn 4633 . . 3  wff  F  Fn  A
63crn 4627 . . . 4  class  ran  F
76, 2wss 3094 . . 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  5278  feq2  5279  feq3  5280  nff  5290  ffn  5292  dffn2  5293  frn  5298  dffn3  5299  fss  5300  fco  5301  funssxp  5305  fun  5308  fnfco  5310  fssres  5311  fcoi2  5319  fint  5323  fin  5324  f0  5328  fconst  5330  f1ssr  5346  fof  5354  dff1o2  5380  fun11iun  5396  ffoss  5408  dff2  5571  dff3  5572  fmpt  5580  ffnfv  5584  ffvresb  5589  fpr  5603  idref  5658  dff1o6  5690  fliftf  5713  1stcof  6046  2ndcof  6047  smores  6302  smores2  6304  iordsmo  6307  map0e  6738  sbthlem9  6912  sucdom2  6990  inf3lem6  7267  alephsmo  7662  alephsing  7835  axdc3lem2  8010  smobeth  8141  fpwwe2lem11  8195  gch3  8235  gruiun  8354  gruima  8357  nqerf  8487  om2uzf1oi  10947  fclim  11957  invf  13597  funcres2b  13698  funcres2c  13702  hofcllem  13959  hofcl  13960  resmhm2b  14365  gsumval2  14387  frmdss2  14412  gsumval3a  15116  subgdmdprd  15196  cnrest  16940  cnrest2  16941  lmss  16953  concn  17079  txflf  17628  clsnsg  17719  tgpconcomp  17722  causs  18651  ellimc2  19154  perfdvf  19180  c1lip2  19272  dvne0  19285  plyeq0  19520  plyreres  19590  aannenlem1  19635  taylf  19667  ulmss  19701  hhssnv  21766  pjfi  22226  fdmrn  22961  cvmlift2lem9a  23171  elno2  23641  elno3  23642  axdenselem6  23674  mptelee  23863  domrancur1b  24532  trnij  24947  fnckleb  25378  isbnd3  25840  lsslindf  26632  indlcim  26642  dvsid  26880  fnvinran  27018  cncmpmax  27036  stoweidlem27  27076  stoweidlem29  27078  stoweidlem31  27080  dihf11lem  30586
  Copyright terms: Public domain W3C validator