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

Theorem fdm 5393
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fdm  |-  ( F : A --> B  ->  dom  F  =  A )

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5389 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5343 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 15 1  |-  ( F : A --> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   dom cdm 4689    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  fdmi  5394  fssxp  5400  ffdm  5403  dmfex  5424  f00  5426  foima  5456  foco  5461  resdif  5494  fimacnv  5657  dff3  5673  ffvresb  5690  fmptco  5691  fornex  5750  onnseq  6361  issmo2  6366  smoiso  6379  mapprc  6776  elpm2r  6788  map0b  6806  mapsn  6809  brdomg  6872  pw2f1olem  6966  fopwdom  6970  fodomfib  7136  intrnfi  7170  ordtypelem5  7237  ordtypelem6  7238  ordtypelem7  7239  ordtypelem8  7240  wemapso2  7267  brwdomn0  7283  wdomtr  7289  cantnfcl  7368  cantnfle  7372  cantnflt  7373  cantnff  7375  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cantnflem3  7393  cnfcomlem  7402  cnfcom  7403  cnfcom2lem  7404  cnfcom3lem  7406  cnfcom3  7407  iunmapdisj  7650  fseqenlem2  7652  fodomfi2  7687  infmap2  7844  coftr  7899  fin23lem30  7968  fin23lem40  7977  isf34lem5  8004  isf34lem7  8005  isf34lem6  8006  fin1a2lem7  8032  axdc3lem2  8077  axdc3lem4  8079  ttukeylem6  8141  fodomb  8151  pwxpndom2  8287  nn0supp  10017  rpnnen1lem4  10345  rpnnen1lem5  10346  fseqsupcl  11039  fseqsupubi  11040  hashf1lem1  11393  swrdcl  11452  swrdval2  11453  cats1un  11476  limsupgle  11951  limsupgre  11955  rlim  11969  rlimi  11987  ello12  11990  lo1bdd  11994  elo12  12001  o1bdd  12005  lo1o1  12006  rlimclim  12020  rlimuni  12024  lo1eq  12042  rlimeq  12043  rlimcld2  12052  o1co  12060  rlimcn1  12062  rlimcn2  12064  rlimsqzlem  12122  isercolllem2  12139  isercolllem3  12140  fsumss  12198  ruclem11  12518  1arith  12974  vdwlem1  13028  vdwlem5  13032  vdwlem6  13033  vdwlem11  13038  ramval  13055  0ram  13067  0ram2  13068  0ramcl  13070  mrcuni  13523  homarcl2  13867  prfval  13973  fisuppfi  14450  gsumval  14452  gsumval2  14460  ghmrn  14696  ghmpreima  14704  cntzmhm2  14815  gsumval3  15191  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumzmhm  15210  gsumzoppg  15216  gsum2d  15223  dmdprdd  15237  dprdres  15263  dprdss  15264  dprdz  15265  dprdf1  15268  dmdprdsplitlem  15272  dprd2da  15277  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dmdprdsplit  15282  dprdsplit  15283  dpjidcl  15293  ablfac1eulem  15307  ablfac1eu  15308  ablfaclem2  15321  ablfaclem3  15322  ablfac2  15324  lmhmpreima  15805  lmhmlsp  15806  mplcoe1  16209  mplcoe2  16211  psr1baslem  16264  gsumfsum  16439  pjdm2  16611  iinopn  16648  iscnp3  16974  lmbrf  16990  cnpnei  16993  cnclima  16997  iscncl  16998  cnntri  17000  cnclsi  17001  cncls2  17002  cncls  17003  cnntr  17004  cncnp  17009  cnrest  17013  cndis  17019  paste  17022  lmcnp  17032  cnt0  17074  cnt1  17078  cnhaus  17082  cncmp  17119  imacmp  17124  hauscmplem  17133  cnconn  17148  conima  17151  1stcfb  17171  1stccnp  17188  1stckgenlem  17248  kgencn  17251  kgencn3  17253  txcnpi  17302  txcnp  17314  txcnmpt  17318  prdstps  17323  xkohaus  17347  xkopt  17349  xkoco2cn  17352  xkococnlem  17353  qtopval2  17387  qtopcn  17405  qtopeu  17407  hmeores  17462  fbasrn  17579  fmval  17638  fmf  17640  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  cnflf2  17698  lmflf  17700  txflf  17701  alexsublem  17738  clssubg  17791  ghmcnp  17797  tgphaus  17799  divstgplem  17803  tsmsval  17813  tsmsgsum  17821  xmetdmdm  17900  metn0  17924  xmetres  17928  metres  17929  xmeter  17979  tmsval  18027  metcnp  18087  isngp2  18119  evth  18457  lmmbrf  18688  iscfil2  18692  caufval  18701  iscau2  18703  iscauf  18706  caucfil  18709  cmetcaulem  18714  equivcau  18726  lmclimf  18729  minveclem3b  18792  ovollb2  18848  ovolunlem1a  18855  ovoliunlem1  18861  ovoliun2  18865  ioombl1lem4  18918  uniioombllem1  18936  uniioombllem2  18938  uniioombllem6  18943  mbfconstlem  18984  ismbf  18985  ismbfcn  18986  mbfimaicc  18988  mbfmulc2lem  19002  mbfmulc2re  19003  mbfneg  19005  mbfimaopn2  19012  cncombf  19013  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  mbflimsup  19021  i1f0rn  19037  itg1addlem5  19055  itg1climres  19069  mbfmullem2  19079  itg2monolem1  19105  itg2mono  19108  itg2i1fseq2  19111  itg2cnlem1  19116  isibl2  19121  ibl0  19141  cniccibl  19195  limcfval  19222  limcdif  19226  ellimc2  19227  ellimc3  19229  limccnp  19241  limccnp2  19242  limcco  19243  dvfval  19247  cpnord  19284  cpnres  19286  dvcmul  19293  dvcmulf  19294  dvnfre  19301  dvexp  19302  c1liplem1  19343  c1lip2  19345  dvgt0lem1  19349  dvcnvrelem1  19364  dvcnvrelem2  19365  itgsubstlem  19395  mdegfval  19448  mdegleb  19450  mdegldg  19452  deg1mul3le  19502  plyco0  19574  plyeq0lem  19592  plyeq0  19593  plyaddlem1  19595  plymullem1  19596  dgrcl  19615  dgrub  19616  dgrlb  19618  plycpn  19669  vieta1lem1  19690  vieta1lem2  19691  aalioulem3  19714  taylfvallem1  19736  tayl0  19741  taylply2  19747  taylply  19748  dvtaylp  19749  dvntaylp  19750  dvntaylp0  19751  taylthlem1  19752  taylthlem2  19753  ulm2  19764  ulmss  19774  ulmdvlem1  19777  ulmdvlem2  19778  ulmdvlem3  19779  iblulm  19783  itgulm  19784  rlimcnp2  20261  xrlimcnp  20263  basellem5  20322  dchrelbas2  20476  dchrghm  20495  dchrptlem1  20503  dchrptlem2  20504  dchrisumlema  20637  grporndm  20877  resgrprn  20947  isabloda  20966  subgores  20971  ismgm  20987  ismndo2  21012  ghsubgolem  21037  rngodm1dm2  21085  rngosn3  21093  vcoprne  21135  nvdm  21227  sspn  21312  htthlem  21497  dmadjrnb  22486  elnlfn  22508  dmhashres  23174  xppreima  23211  fmptcof2  23229  curry2ima  23247  xrofsup  23255  rge0scvg  23373  esumpcvgval  23446  ofcfval4  23466  isrnmeas  23531  measdivcst  23552  indpreima  23608  indf1ofs  23609  rrvdm  23649  coinfliprv  23683  cvmliftmolem1  23812  cvmliftlem3  23818  cvmliftlem10  23825  cvmliftlem13  23827  cvmlift2lem9  23842  cvmlift3lem6  23855  cvmlift3lem7  23856  wrdumgra  23868  umgra1  23878  umgraun  23879  eupares  23899  ghomfo  23998  soseq  24254  nodmon  24304  eedimeq  24526  axcontlem10  24601  islatalg  25183  dmrngrp  25339  mgmrddd  25366  rngmgmbs3  25417  rngodmeqrn  25419  zintdom  25438  svs3  25488  intopcoaconlem3b  25538  intopcoaconlem3  25539  istopx  25547  cmptdst  25568  flfnei2  25577  islimrs4  25582  bwt2  25592  lvsovso  25626  supnuf  25629  dcsda  25733  morcat  25780  domdomcatfun  25926  obcatset  25942  domidcat  25945  indcls2  25996  ivthALT  26258  indexdom  26413  sdclem2  26452  cnres2  26483  sstotbnd2  26498  isbnd3  26508  ssbnd  26512  bnd2lem  26515  ismtyval  26524  exidreslem  26567  grpokerinj  26575  divrngcl  26588  isdrngo2  26589  keridl  26657  ismrcd1  26773  istopclsd  26775  mapfzcons2  26796  coeq0i  26832  pw2f1ocnv  27130  fnwe2lem2  27148  lmhmfgima  27182  fsuppeq  27259  pwfi2f1o  27260  islindf2  27284  f1lindf  27292  f1omvdconj  27389  pmtrfconj  27407  expgrowth  27552  cncmpmax  27703  stoweidlem29  27778  uslgraun  28120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator