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

Theorem fdm 5409
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 5405 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5359 . 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 1632   dom cdm 4705    Fn wfn 5266   -->wf 5267
This theorem is referenced by:  fdmi  5410  fssxp  5416  ffdm  5419  dmfex  5440  f00  5442  foima  5472  foco  5477  resdif  5510  fimacnv  5673  dff3  5689  ffvresb  5706  fmptco  5707  fornex  5766  onnseq  6377  issmo2  6382  smoiso  6395  mapprc  6792  elpm2r  6804  map0b  6822  mapsn  6825  brdomg  6888  pw2f1olem  6982  fopwdom  6986  fodomfib  7152  intrnfi  7186  ordtypelem5  7253  ordtypelem6  7254  ordtypelem7  7255  ordtypelem8  7256  wemapso2  7283  brwdomn0  7299  wdomtr  7305  cantnfcl  7384  cantnfle  7388  cantnflt  7389  cantnff  7391  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  cantnflem3  7409  cnfcomlem  7418  cnfcom  7419  cnfcom2lem  7420  cnfcom3lem  7422  cnfcom3  7423  iunmapdisj  7666  fseqenlem2  7668  fodomfi2  7703  infmap2  7860  coftr  7915  fin23lem30  7984  fin23lem40  7993  isf34lem5  8020  isf34lem7  8021  isf34lem6  8022  fin1a2lem7  8048  axdc3lem2  8093  axdc3lem4  8095  ttukeylem6  8157  fodomb  8167  pwxpndom2  8303  nn0supp  10033  rpnnen1lem4  10361  rpnnen1lem5  10362  fseqsupcl  11055  fseqsupubi  11056  hashf1lem1  11409  swrdcl  11468  swrdval2  11469  cats1un  11492  limsupgle  11967  limsupgre  11971  rlim  11985  rlimi  12003  ello12  12006  lo1bdd  12010  elo12  12017  o1bdd  12021  lo1o1  12022  rlimclim  12036  rlimuni  12040  lo1eq  12058  rlimeq  12059  rlimcld2  12068  o1co  12076  rlimcn1  12078  rlimcn2  12080  rlimsqzlem  12138  isercolllem2  12155  isercolllem3  12156  fsumss  12214  ruclem11  12534  1arith  12990  vdwlem1  13044  vdwlem5  13048  vdwlem6  13049  vdwlem11  13054  ramval  13071  0ram  13083  0ram2  13084  0ramcl  13086  mrcuni  13539  homarcl2  13883  prfval  13989  fisuppfi  14466  gsumval  14468  gsumval2  14476  ghmrn  14712  ghmpreima  14720  cntzmhm2  14831  gsumval3  15207  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumzmhm  15226  gsumzoppg  15232  gsum2d  15239  dmdprdd  15253  dprdres  15279  dprdss  15280  dprdz  15281  dprdf1  15284  dmdprdsplitlem  15288  dprd2da  15293  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dmdprdsplit  15298  dprdsplit  15299  dpjidcl  15309  ablfac1eulem  15323  ablfac1eu  15324  ablfaclem2  15337  ablfaclem3  15338  ablfac2  15340  lmhmpreima  15821  lmhmlsp  15822  mplcoe1  16225  mplcoe2  16227  psr1baslem  16280  gsumfsum  16455  pjdm2  16627  iinopn  16664  iscnp3  16990  lmbrf  17006  cnpnei  17009  cnclima  17013  iscncl  17014  cnntri  17016  cnclsi  17017  cncls2  17018  cncls  17019  cnntr  17020  cncnp  17025  cnrest  17029  cndis  17035  paste  17038  lmcnp  17048  cnt0  17090  cnt1  17094  cnhaus  17098  cncmp  17135  imacmp  17140  hauscmplem  17149  cnconn  17164  conima  17167  1stcfb  17187  1stccnp  17204  1stckgenlem  17264  kgencn  17267  kgencn3  17269  txcnpi  17318  txcnp  17330  txcnmpt  17334  prdstps  17339  xkohaus  17363  xkopt  17365  xkoco2cn  17368  xkococnlem  17369  qtopval2  17403  qtopcn  17421  qtopeu  17423  hmeores  17478  fbasrn  17595  fmval  17654  fmf  17656  rnelfmlem  17663  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  cnflf2  17714  lmflf  17716  txflf  17717  alexsublem  17754  clssubg  17807  ghmcnp  17813  tgphaus  17815  divstgplem  17819  tsmsval  17829  tsmsgsum  17837  xmetdmdm  17916  metn0  17940  xmetres  17944  metres  17945  xmeter  17995  tmsval  18043  metcnp  18103  isngp2  18135  evth  18473  lmmbrf  18704  iscfil2  18708  caufval  18717  iscau2  18719  iscauf  18722  caucfil  18725  cmetcaulem  18730  equivcau  18742  lmclimf  18745  minveclem3b  18808  ovollb2  18864  ovolunlem1a  18871  ovoliunlem1  18877  ovoliun2  18881  ioombl1lem4  18934  uniioombllem1  18952  uniioombllem2  18954  uniioombllem6  18959  mbfconstlem  19000  ismbf  19001  ismbfcn  19002  mbfimaicc  19004  mbfmulc2lem  19018  mbfmulc2re  19019  mbfneg  19021  mbfimaopn2  19028  cncombf  19029  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  mbflimsup  19037  i1f0rn  19053  itg1addlem5  19071  itg1climres  19085  mbfmullem2  19095  itg2monolem1  19121  itg2mono  19124  itg2i1fseq2  19127  itg2cnlem1  19132  isibl2  19137  ibl0  19157  cniccibl  19211  limcfval  19238  limcdif  19242  ellimc2  19243  ellimc3  19245  limccnp  19257  limccnp2  19258  limcco  19259  dvfval  19263  cpnord  19300  cpnres  19302  dvcmul  19309  dvcmulf  19310  dvnfre  19317  dvexp  19318  c1liplem1  19359  c1lip2  19361  dvgt0lem1  19365  dvcnvrelem1  19380  dvcnvrelem2  19381  itgsubstlem  19411  mdegfval  19464  mdegleb  19466  mdegldg  19468  deg1mul3le  19518  plyco0  19590  plyeq0lem  19608  plyeq0  19609  plyaddlem1  19611  plymullem1  19612  dgrcl  19631  dgrub  19632  dgrlb  19634  plycpn  19685  vieta1lem1  19706  vieta1lem2  19707  aalioulem3  19730  taylfvallem1  19752  tayl0  19757  taylply2  19763  taylply  19764  dvtaylp  19765  dvntaylp  19766  dvntaylp0  19767  taylthlem1  19768  taylthlem2  19769  ulm2  19780  ulmss  19790  ulmdvlem1  19793  ulmdvlem2  19794  ulmdvlem3  19795  iblulm  19799  itgulm  19800  rlimcnp2  20277  xrlimcnp  20279  basellem5  20338  dchrelbas2  20492  dchrghm  20511  dchrptlem1  20519  dchrptlem2  20520  dchrisumlema  20653  grporndm  20893  resgrprn  20963  isabloda  20982  subgores  20987  ismgm  21003  ismndo2  21028  ghsubgolem  21053  rngodm1dm2  21101  rngosn3  21109  vcoprne  21151  nvdm  21243  sspn  21328  htthlem  21513  dmadjrnb  22502  elnlfn  22524  dmhashres  23190  xppreima  23226  fmptcof2  23244  curry2ima  23262  xrofsup  23270  rge0scvg  23388  esumpcvgval  23461  ofcfval4  23481  isrnmeas  23546  measdivcst  23567  indpreima  23623  indf1ofs  23624  rrvdm  23664  coinfliprv  23698  cvmliftmolem1  23827  cvmliftlem3  23833  cvmliftlem10  23840  cvmliftlem13  23842  cvmlift2lem9  23857  cvmlift3lem6  23870  cvmlift3lem7  23871  wrdumgra  23883  umgra1  23893  umgraun  23894  eupares  23914  ghomfo  24013  soseq  24325  nodmon  24375  eedimeq  24598  axcontlem10  24673  itg2addnclem  25003  itg2addnclem2  25004  cnicciblnc  25022  islatalg  25286  dmrngrp  25442  mgmrddd  25469  rngmgmbs3  25520  rngodmeqrn  25522  zintdom  25541  svs3  25591  intopcoaconlem3b  25641  intopcoaconlem3  25642  istopx  25650  cmptdst  25671  flfnei2  25680  islimrs4  25685  bwt2  25695  lvsovso  25729  supnuf  25732  dcsda  25836  morcat  25883  domdomcatfun  26029  obcatset  26045  domidcat  26048  indcls2  26099  ivthALT  26361  indexdom  26516  sdclem2  26555  cnres2  26586  sstotbnd2  26601  isbnd3  26611  ssbnd  26615  bnd2lem  26618  ismtyval  26627  exidreslem  26670  grpokerinj  26678  divrngcl  26691  isdrngo2  26692  keridl  26760  ismrcd1  26876  istopclsd  26878  mapfzcons2  26899  coeq0i  26935  pw2f1ocnv  27233  fnwe2lem2  27251  lmhmfgima  27285  fsuppeq  27362  pwfi2f1o  27363  islindf2  27387  f1lindf  27395  f1omvdconj  27492  pmtrfconj  27510  expgrowth  27655  cncmpmax  27806  stoweidlem29  27881  uslgraun  28254
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 5274  df-f 5275
  Copyright terms: Public domain W3C validator