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

Theorem fdm 5584
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 5580 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5531 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 16 1  |-  ( F : A --> B  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   dom cdm 4861    Fn wfn 5434   -->wf 5435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-fn 5442  df-f 5443
This theorem is referenced by:  fdmi  5585  fssxp  5591  ffdm  5593  f00  5614  f0dom0  5616  foima  5646  foco  5651  resdif  5682  fimacnv  5856  dff3  5877  ffvresb  5895  fmptco  5897  dmfex  6556  fornex  6567  frnsuppeq  6723  suppss  6740  onnseq  6826  issmo2  6831  smoiso  6844  mapprc  7239  elpm2r  7251  map0b  7272  mapsn  7275  brdomg  7341  pw2f1olem  7436  fopwdom  7440  fodomfib  7612  fisuppfi  7649  intrnfi  7687  ordtypelem5  7757  ordtypelem6  7758  ordtypelem7  7759  ordtypelem8  7760  wemapso2OLD  7787  wemapso2lem  7788  brwdomn0  7805  wdomtr  7811  cantnfcl  7896  cantnfle  7900  cantnflt  7901  cantnff  7903  cantnfp1lem2  7908  cantnfp1lem3  7909  cantnflem1b  7915  cantnflem1d  7917  cantnflem1  7918  cantnflem3  7920  cantnfclOLD  7926  cantnfleOLD  7930  cantnfltOLD  7931  cantnfp1lem2OLD  7934  cantnfp1lem3OLD  7935  cantnflem1bOLD  7938  cantnflem1dOLD  7940  cantnflem1OLD  7941  cantnflem3OLD  7942  cnfcomlem  7953  cnfcom  7954  cnfcom2lem  7955  cnfcom3lem  7957  cnfcom3  7958  cnfcomlemOLD  7961  cnfcomOLD  7962  cnfcom2lemOLD  7963  cnfcom3lemOLD  7965  cnfcom3OLD  7966  iunmapdisj  8214  fseqenlem2  8216  fodomfi2  8251  infmap2  8408  coftr  8463  fin23lem30  8532  fin23lem40  8541  isf34lem5  8568  isf34lem7  8569  isf34lem6  8570  fin1a2lem7  8596  axdc3lem2  8641  axdc3lem4  8643  ttukeylem6  8704  fodomb  8714  pwxpndom2  8853  nn0suppOLD  10655  rpnnen1lem4  11003  rpnnen1lem5  11004  fseqsupcl  11820  fseqsupubi  11821  hashimarn  12221  hashfzdm  12223  hashfirdm  12225  hashf1lem1  12229  wrdsymb0  12280  lsw0  12288  swrdcl  12336  swrdval2  12337  swrdnd  12347  swrdvalodm2  12354  swrdvalodm  12355  cats1un  12391  repswswrd  12443  limsupgle  12976  limsupgre  12980  rlim  12994  rlimi  13012  ello12  13015  lo1bdd  13019  elo12  13026  o1bdd  13030  lo1o1  13031  rlimclim  13045  rlimuni  13049  lo1eq  13067  rlimeq  13068  rlimcld2  13077  o1co  13085  rlimcn1  13087  rlimcn2  13089  rlimsqzlem  13147  isercolllem2  13164  isercolllem3  13165  fsumss  13223  ruclem11  13543  1arith  14009  vdwlem1  14063  vdwlem5  14067  vdwlem6  14068  vdwlem11  14073  ramval  14090  0ram  14102  0ram2  14103  0ramcl  14105  mrcuni  14580  homarcl2  14924  prfval  15030  gsumval  15524  gsumval2  15534  ghmrn  15781  ghmpreima  15789  cntzmhm2  15878  symgfixf1  15964  f1omvdconj  15973  pmtrfconj  15993  pmtrdifellem1  16003  pmtrdifellem2  16004  gsumval3OLD  16403  gsumval3lem1  16404  gsumval3lem2  16405  gsumval3  16406  gsumzres  16409  gsumzcl2  16410  gsumzf1o  16412  gsumzresOLD  16413  gsumzclOLD  16414  gsumzf1oOLD  16415  gsumzaddlem  16429  gsumzaddlemOLD  16431  gsumzmhm  16452  gsumzmhmOLD  16453  gsumzoppg  16462  gsumzoppgOLD  16463  gsum2d  16485  gsum2dOLD  16486  dmdprdd  16503  dprdres  16547  dprdss  16548  dprdz  16549  dprdf1  16552  dmdprdsplitlem  16556  dmdprdsplitlemOLD  16557  dprd2da  16563  dmdprdsplit2lem  16566  dmdprdsplit2  16567  dmdprdsplit  16568  dprdsplit  16569  dpjidcl  16579  dpjidclOLD  16586  ablfac1eulem  16595  ablfac1eu  16596  ablfaclem2  16609  ablfaclem3  16610  ablfac2  16612  lmhmpreima  17151  lmhmlsp  17152  mplcoe1  17566  mplcoe5  17570  mplcoe2OLD  17572  psr1baslem  17663  gsumfsum  17901  evpmss  18038  regsumsupp  18074  pjdm2  18158  frlmlbs  18247  islindf2  18265  f1lindf  18273  islindf4  18289  mattpostpos  18360  mdet1  18430  iinopn  18537  iscnp3  18870  lmbrf  18886  cnpnei  18890  cnclima  18894  iscncl  18895  cnntri  18897  cnclsi  18898  cncls2  18899  cncls  18900  cnntr  18901  cncnp  18906  cnrest  18911  cndis  18917  paste  18920  lmcnp  18930  cnt0  18972  cnt1  18976  cnhaus  18980  cncmp  19017  imacmp  19022  hauscmplem  19031  bwthOLD  19036  cnconn  19048  conima  19051  1stcfb  19071  1stccnp  19088  1stckgenlem  19148  kgencn  19151  kgencn3  19153  txcnpi  19203  txcnp  19215  txcnmpt  19219  prdstps  19224  xkohaus  19248  xkopt  19250  xkoco2cn  19253  xkococnlem  19254  qtopval2  19291  qtopcn  19309  qtopeu  19311  hmeores  19366  fbasrn  19479  fmval  19538  fmf  19540  rnelfmlem  19547  rnelfm  19548  fmfnfmlem2  19550  fmfnfmlem4  19552  fmfnfm  19553  cnflf2  19598  lmflf  19600  txflf  19601  alexsublem  19638  cnextfval  19656  cnextcn  19661  clssubg  19701  ghmcnp  19707  tgphaus  19709  divstgplem  19713  tsmsval  19723  tsmsgsum  19731  tsmsgsumOLD  19734  ucncn  19882  psmetdmdm  19903  xmetdmdm  19932  metn0  19957  xmetres  19961  metres  19962  xmeter  20030  tmsval  20078  metcnp  20138  metustssOLD  20150  metustss  20151  metustidOLD  20156  metustid  20157  metustsymOLD  20158  metustsym  20159  metustexhalfOLD  20160  metustexhalf  20161  metustfbasOLD  20162  metustfbas  20163  cfilucfilOLD  20166  cfilucfil  20167  metuel2  20176  restmetu  20184  isngp2  20211  evth  20553  lmmbrf  20795  iscfil2  20799  caufval  20808  iscau2  20810  iscauf  20813  caucfil  20816  cmetcaulem  20821  equivcau  20833  lmclimf  20836  rrxcph  20918  rrxsuppss  20924  minveclem3b  20937  ovollb2  20994  ovolunlem1a  21001  ovoliunlem1  21007  ovoliun2  21011  ioombl1lem4  21064  uniioombllem1  21083  uniioombllem2  21085  uniioombllem6  21090  mbfconstlem  21129  ismbf  21130  ismbfcn  21131  mbfimaicc  21133  mbfmulc2lem  21147  mbfmulc2re  21148  mbfneg  21150  mbfimaopn2  21157  cncombf  21158  mbfaddlem  21160  mbfsup  21164  mbfinf  21165  mbflimsup  21166  i1f0rn  21182  itg1addlem5  21200  itg1climres  21214  mbfmullem2  21224  itg2monolem1  21250  itg2mono  21253  itg2i1fseq2  21256  itg2cnlem1  21261  isibl2  21266  ibl0  21286  cniccibl  21340  limcfval  21369  limcdif  21373  ellimc2  21374  ellimc3  21376  limccnp  21388  limccnp2  21389  limcco  21390  dvfval  21394  cpnord  21431  cpnres  21433  dvcmul  21440  dvcmulf  21441  dvnfre  21448  dvexp  21449  c1liplem1  21490  c1lip2  21492  dvgt0lem1  21496  dvcnvrelem1  21511  dvcnvrelem2  21512  itgsubstlem  21542  mdegfval  21553  mdegleb  21557  mdegldg  21559  deg1mul3le  21610  plyco0  21682  plyeq0lem  21700  plyeq0  21701  plyaddlem1  21703  plymullem1  21704  dgrcl  21723  dgrub  21724  dgrlb  21726  plycpn  21777  vieta1lem1  21798  vieta1lem2  21799  aalioulem3  21822  taylfvallem1  21844  tayl0  21849  taylply2  21855  taylply  21856  dvtaylp  21857  dvntaylp  21858  dvntaylp0  21859  taylthlem1  21860  taylthlem2  21861  ulm2  21872  ulmss  21884  ulmdvlem1  21887  ulmdvlem2  21888  ulmdvlem3  21889  iblulm  21894  itgulm  21895  rlimcnp2  22382  xrlimcnp  22384  basellem5  22444  dchrelbas2  22598  dchrghm  22617  dchrptlem1  22625  dchrptlem2  22626  dchrisumlema  22759  iscgrgd  22988  trgcgrg  22989  eedimeq  23166  axcontlem10  23241  uhgraun  23267  wrdumgra  23272  umgra1  23282  umgraun  23284  eupares  23618  grporndm  23719  resgrprn  23789  isabloda  23808  subgores  23813  ismgm  23829  ismndo2  23854  ghsubgolem  23879  rngodm1dm2  23927  rngosn3  23935  vcoprne  23979  nvdm  24071  sspn  24156  htthlem  24341  dmadjrnb  25332  elnlfn  25354  xppreima  25986  fmptcof2  26001  curry2ima  26025  fpwrelmap  26055  hauseqcn  26347  rge0scvg  26401  indpreima  26503  indf1ofs  26504  esumpcvgval  26549  ofcfval4  26569  isrnmeas  26636  measdivcst  26661  omsfval  26731  oms0  26732  omsmon  26733  sibfof  26748  sitgclg  26750  eulerpartlemsv2  26763  eulerpartlemsf  26764  eulerpartlemv  26769  eulerpartlemd  26771  eulerpartlemb  26773  eulerpartlemt  26776  eulerpartlemr  26779  eulerpartlemgvv  26781  eulerpartlemgu  26782  eulerpartlemgs2  26785  eulerpartlemn  26786  sseqfv2  26799  rrvdm  26851  cvmliftmolem1  27192  cvmliftlem3  27198  cvmliftlem10  27205  cvmliftlem13  27207  cvmlift2lem9  27222  cvmlift3lem6  27235  cvmlift3lem7  27236  ghomfo  27332  fprodss  27483  soseq  27737  nodmon  27813  heicant  28452  mbfresfi  28464  itg2addnclem  28469  itg2addnclem2  28470  cnicciblnc  28489  ftc1anclem1  28493  ftc1anclem5  28497  ftc1anclem6  28498  ftc1anclem8  28500  ivthALT  28556  indexdom  28654  sdclem2  28664  cnres2  28688  sstotbnd2  28699  isbnd3  28709  ssbnd  28713  bnd2lem  28716  ismtyval  28725  exidreslem  28768  grpokerinj  28776  divrngcl  28789  isdrngo2  28790  keridl  28858  ismrcd1  29060  istopclsd  29062  mapfzcons2  29081  coeq0i  29117  pw2f1ocnv  29412  fnwe2lem2  29430  lmhmfgima  29463  fsuppeq  29476  pwfi2f1o  29477  cnioobibld  29615  itgpowd  29616  expgrowth  29635  cncmpmax  29780  stoweidlem29  29850  f0rn0  30167  wlkn0  30305  domnmsuppn0  30812  rmsuppss  30813  mndpsuppss  30814  scmsuppss  30815  mdetdiaglem  30932  bj-finsumval0  32679
  Copyright terms: Public domain W3C validator