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

Theorem fdm 5597
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 5593 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5546 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 16 1  |-  ( F : A --> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   dom cdm 4880    Fn wfn 5451   -->wf 5452
This theorem is referenced by:  fdmi  5598  fssxp  5604  ffdm  5607  dmfex  5628  f00  5630  foima  5660  foco  5665  resdif  5698  fimacnv  5864  dff3  5884  ffvresb  5902  fmptco  5903  fornex  5972  onnseq  6608  issmo2  6613  smoiso  6626  mapprc  7024  elpm2r  7036  map0b  7054  mapsn  7057  brdomg  7120  pw2f1olem  7214  fopwdom  7218  fodomfib  7388  intrnfi  7423  ordtypelem5  7493  ordtypelem6  7494  ordtypelem7  7495  ordtypelem8  7496  wemapso2  7523  brwdomn0  7539  wdomtr  7545  cantnfcl  7624  cantnfle  7628  cantnflt  7629  cantnff  7631  cantnfp1lem2  7637  cantnfp1lem3  7638  cantnflem1b  7644  cantnflem1d  7646  cantnflem1  7647  cantnflem3  7649  cnfcomlem  7658  cnfcom  7659  cnfcom2lem  7660  cnfcom3lem  7662  cnfcom3  7663  iunmapdisj  7906  fseqenlem2  7908  fodomfi2  7943  infmap2  8100  coftr  8155  fin23lem30  8224  fin23lem40  8233  isf34lem5  8260  isf34lem7  8261  isf34lem6  8262  fin1a2lem7  8288  axdc3lem2  8333  axdc3lem4  8335  ttukeylem6  8396  fodomb  8406  pwxpndom2  8542  nn0supp  10275  rpnnen1lem4  10605  rpnnen1lem5  10606  fseqsupcl  11318  fseqsupubi  11319  hashf1lem1  11706  swrdcl  11768  swrdval2  11769  cats1un  11792  limsupgle  12273  limsupgre  12277  rlim  12291  rlimi  12309  ello12  12312  lo1bdd  12316  elo12  12323  o1bdd  12327  lo1o1  12328  rlimclim  12342  rlimuni  12346  lo1eq  12364  rlimeq  12365  rlimcld2  12374  o1co  12382  rlimcn1  12384  rlimcn2  12386  rlimsqzlem  12444  isercolllem2  12461  isercolllem3  12462  fsumss  12521  ruclem11  12841  1arith  13297  vdwlem1  13351  vdwlem5  13355  vdwlem6  13356  vdwlem11  13361  ramval  13378  0ram  13390  0ram2  13391  0ramcl  13393  mrcuni  13848  homarcl2  14192  prfval  14298  fisuppfi  14775  gsumval  14777  gsumval2  14785  ghmrn  15021  ghmpreima  15029  cntzmhm2  15140  gsumval3  15516  gsumzres  15519  gsumzcl  15520  gsumzf1o  15521  gsumzaddlem  15528  gsumzmhm  15535  gsumzoppg  15541  gsum2d  15548  dmdprdd  15562  dprdres  15588  dprdss  15589  dprdz  15590  dprdf1  15593  dmdprdsplitlem  15597  dprd2da  15602  dmdprdsplit2lem  15605  dmdprdsplit2  15606  dmdprdsplit  15607  dprdsplit  15608  dpjidcl  15618  ablfac1eulem  15632  ablfac1eu  15633  ablfaclem2  15646  ablfaclem3  15647  ablfac2  15649  lmhmpreima  16126  lmhmlsp  16127  mplcoe1  16530  mplcoe2  16532  psr1baslem  16585  gsumfsum  16768  pjdm2  16940  iinopn  16977  iscnp3  17310  lmbrf  17326  cnpnei  17330  cnclima  17334  iscncl  17335  cnntri  17337  cnclsi  17338  cncls2  17339  cncls  17340  cnntr  17341  cncnp  17346  cnrest  17351  cndis  17357  paste  17360  lmcnp  17370  cnt0  17412  cnt1  17416  cnhaus  17420  cncmp  17457  imacmp  17462  hauscmplem  17471  bwth  17475  cnconn  17487  conima  17490  1stcfb  17510  1stccnp  17527  1stckgenlem  17587  kgencn  17590  kgencn3  17592  txcnpi  17642  txcnp  17654  txcnmpt  17658  prdstps  17663  xkohaus  17687  xkopt  17689  xkoco2cn  17692  xkococnlem  17693  qtopval2  17730  qtopcn  17748  qtopeu  17750  hmeores  17805  fbasrn  17918  fmval  17977  fmf  17979  rnelfmlem  17986  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem4  17991  fmfnfm  17992  cnflf2  18037  lmflf  18039  txflf  18040  alexsublem  18077  cnextfval  18095  cnextcn  18100  clssubg  18140  ghmcnp  18146  tgphaus  18148  divstgplem  18152  tsmsval  18162  tsmsgsum  18170  ucncn  18317  psmetdmdm  18338  xmetdmdm  18367  metn0  18392  xmetres  18396  metres  18397  xmeter  18465  tmsval  18513  metcnp  18573  metustssOLD  18585  metustss  18586  metustidOLD  18591  metustid  18592  metustsymOLD  18593  metustsym  18594  metustexhalfOLD  18595  metustexhalf  18596  metustfbasOLD  18597  metustfbas  18598  cfilucfilOLD  18601  cfilucfil  18602  metuel2  18611  restmetu  18619  isngp2  18646  evth  18986  lmmbrf  19217  iscfil2  19221  caufval  19230  iscau2  19232  iscauf  19235  caucfil  19238  cmetcaulem  19243  equivcau  19255  lmclimf  19258  minveclem3b  19331  ovollb2  19387  ovolunlem1a  19394  ovoliunlem1  19400  ovoliun2  19404  ioombl1lem4  19457  uniioombllem1  19475  uniioombllem2  19477  uniioombllem6  19482  mbfconstlem  19523  ismbf  19524  ismbfcn  19525  mbfimaicc  19527  mbfmulc2lem  19541  mbfmulc2re  19542  mbfneg  19544  mbfimaopn2  19551  cncombf  19552  mbfaddlem  19554  mbfsup  19558  mbfinf  19559  mbflimsup  19560  i1f0rn  19576  itg1addlem5  19594  itg1climres  19608  mbfmullem2  19618  itg2monolem1  19644  itg2mono  19647  itg2i1fseq2  19650  itg2cnlem1  19655  isibl2  19660  ibl0  19680  cniccibl  19734  limcfval  19761  limcdif  19765  ellimc2  19766  ellimc3  19768  limccnp  19780  limccnp2  19781  limcco  19782  dvfval  19786  cpnord  19823  cpnres  19825  dvcmul  19832  dvcmulf  19833  dvnfre  19840  dvexp  19841  c1liplem1  19882  c1lip2  19884  dvgt0lem1  19888  dvcnvrelem1  19903  dvcnvrelem2  19904  itgsubstlem  19934  mdegfval  19987  mdegleb  19989  mdegldg  19991  deg1mul3le  20041  plyco0  20113  plyeq0lem  20131  plyeq0  20132  plyaddlem1  20134  plymullem1  20135  dgrcl  20154  dgrub  20155  dgrlb  20157  plycpn  20208  vieta1lem1  20229  vieta1lem2  20230  aalioulem3  20253  taylfvallem1  20275  tayl0  20280  taylply2  20286  taylply  20287  dvtaylp  20288  dvntaylp  20289  dvntaylp0  20290  taylthlem1  20291  taylthlem2  20292  ulm2  20303  ulmss  20315  ulmdvlem1  20318  ulmdvlem2  20319  ulmdvlem3  20320  iblulm  20325  itgulm  20326  rlimcnp2  20807  xrlimcnp  20809  basellem5  20869  dchrelbas2  21023  dchrghm  21042  dchrptlem1  21050  dchrptlem2  21051  dchrisumlema  21184  uhgraun  21348  wrdumgra  21353  umgra1  21363  umgraun  21365  eupares  21699  grporndm  21800  resgrprn  21870  isabloda  21889  subgores  21894  ismgm  21910  ismndo2  21935  ghsubgolem  21960  rngodm1dm2  22008  rngosn3  22016  vcoprne  22060  nvdm  22152  sspn  22237  htthlem  22422  dmadjrnb  23411  elnlfn  23433  xppreima  24061  fmptcof2  24078  curry2ima  24099  hauseqcn  24295  rge0scvg  24337  indpreima  24424  indf1ofs  24425  esumpcvgval  24470  ofcfval4  24490  isrnmeas  24556  measdivcst  24581  sibfof  24656  sitgclg  24658  rrvdm  24706  cvmliftmolem1  24970  cvmliftlem3  24976  cvmliftlem10  24983  cvmliftlem13  24985  cvmlift2lem9  25000  cvmlift3lem6  25013  cvmlift3lem7  25014  ghomfo  25104  fprodss  25276  soseq  25531  nodmon  25607  eedimeq  25839  axcontlem10  25914  mbfresfi  26255  itg2addnclem  26258  itg2addnclem2  26259  cnicciblnc  26278  ftc1anclem1  26282  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem8  26289  ivthALT  26340  indexdom  26438  sdclem2  26448  cnres2  26474  sstotbnd2  26485  isbnd3  26495  ssbnd  26499  bnd2lem  26502  ismtyval  26511  exidreslem  26554  grpokerinj  26562  divrngcl  26575  isdrngo2  26576  keridl  26644  ismrcd1  26754  istopclsd  26756  mapfzcons2  26777  coeq0i  26813  pw2f1ocnv  27110  fnwe2lem2  27128  lmhmfgima  27161  fsuppeq  27238  pwfi2f1o  27239  islindf2  27263  f1lindf  27271  f1omvdconj  27368  pmtrfconj  27386  expgrowth  27531  cncmpmax  27681  stoweidlem29  27756  f0rn0  28081  hashimarn  28174  hashfirdm  28176  hashfzdm  28177  wrdsymb0  28190  swrdnd  28204  swrdvalodm2  28210  swrdvalodm  28211  lswrd0  28283  wlkn0  28320
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 179  df-an 362  df-fn 5459  df-f 5460
  Copyright terms: Public domain W3C validator