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

Definition df-f 5609
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 6062, dff3 6063, and dff4 6064. (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 5601 . 2  wff  F : A
--> B
53, 1wfn 5600 . . 3  wff  F  Fn  A
63crn 4857 . . . 4  class  ran  F
76, 2wss 3416 . . 3  wff  ran  F  C_  B
85, 7wa 375 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 189 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  feq1  5736  feq2  5737  feq3  5738  nff  5751  sbcfg  5753  ffn  5755  dffn2  5757  frn  5762  dffn3  5763  fss  5764  fco  5766  funssxp  5769  fdmrn  5771  fun  5773  fnfco  5775  fssres  5776  fcoi2  5785  fint  5789  fin  5790  f0  5791  fconst  5796  f1ssr  5812  fof  5820  dff1o2  5846  dff2  6062  dff3  6063  fmpt  6071  ffnfv  6077  ffvresb  6083  fpr  6101  idref  6176  dff1o6  6204  fliftf  6238  fun11iun  6785  ffoss  6786  1stcof  6853  2ndcof  6854  smores  7102  smores2  7104  iordsmo  7107  sbthlem9  7721  sucdom2  7799  inf3lem6  8169  alephsmo  8564  alephsing  8737  axdc3lem2  8912  smobeth  9042  fpwwe2lem11  9096  gch3  9132  gruiun  9255  gruima  9258  nqerf  9386  om2uzf1oi  12205  fclim  13672  invf  15728  funcres2b  15857  funcres2c  15861  hofcllem  16198  hofcl  16199  gsumval2  16578  resmhm2b  16663  frmdss2  16702  gsumval3a  17592  subgdmdprd  17722  lsslindf  19443  indlcim  19453  cnrest2  20357  lmss  20369  concn  20496  txflf  21076  cnextf  21136  clsnsg  21179  tgpconcomp  21182  psmetxrge0  21384  causs  22323  ellimc2  22888  perfdvf  22914  c1lip2  23006  dvne0  23019  plyeq0  23221  plyreres  23292  aannenlem1  23340  taylf  23372  ulmss  23408  mptelee  24981  ausisusgra  25138  usgraedgrnv  25160  usgraexmplef  25184  cusgrarn  25243  hhssnv  26971  pjfi  27413  maprnin  28368  measdivcstOLD  29097  sitgf  29230  eulerpartlemn  29264  cvmlift2lem9a  30076  elno2  30591  elno3  30592  nodenselem6  30625  icoreresf  31801  poimirlem30  32016  poimirlem31  32017  isbnd3  32162  dihf11lem  34880  dvsid  36725  stoweidlem27  37988  stoweidlem29  37990  stoweidlem29OLD  37991  stoweidlem31  37993  fourierdlem15  38085  ffnafv  38808  iccpartf  38880  ausgrusgrb  39396  ausgrumgri  39398  subuhgr  39504  subupgr  39505  subumgr  39506  subusgr  39507  uhgraedgrnv  40032  resmgmhm2b  40169
  Copyright terms: Public domain W3C validator