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

Theorem fdm 5946
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fdm (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5940 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 5886 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  dom cdm 5024   Fn wfn 5781  wf 5782
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 195  df-an 384  df-fn 5789  df-f 5790
This theorem is referenced by:  fdmi  5947  fssxp  5955  ffdm  5957  f00  5981  f0dom0  5983  f0rn0  5984  foima  6014  foco  6019  resdif  6051  fimacnv  6236  dff3  6261  ffvresb  6282  fmptco  6284  dmfex  6990  fornex  7001  frnsuppeq  7167  suppss  7185  onnseq  7301  issmo2  7306  smoiso  7319  mapprc  7721  elpm2r  7734  map0b  7755  mapsn  7758  brdomg  7824  pw2f1olem  7922  fopwdom  7926  fodomfib  8098  fisuppfi  8139  intrnfi  8178  ordtypelem5  8283  ordtypelem6  8284  ordtypelem7  8285  ordtypelem8  8286  wemapso2lem  8313  brwdomn0  8330  wdomtr  8336  cantnfcl  8420  cantnfle  8424  cantnflt  8425  cantnff  8427  cantnfp1lem3  8433  cantnflem1b  8439  cantnflem1d  8441  cantnflem1  8442  cantnflem3  8444  cnfcomlem  8452  cnfcom  8453  cnfcom2lem  8454  cnfcom3lem  8456  cnfcom3  8457  iunmapdisj  8702  fseqenlem2  8704  fodomfi2  8739  infmap2  8896  coftr  8951  fin23lem30  9020  fin23lem40  9029  isf34lem5  9056  isf34lem7  9057  isf34lem6  9058  fin1a2lem7  9084  axdc3lem2  9129  axdc3lem4  9131  ttukeylem6  9192  fodomb  9202  pwxpndom2  9339  rpnnen1lem4  11645  rpnnen1lem5  11646  rpnnen1lem4OLD  11651  rpnnen1lem5OLD  11652  fseqsupcl  12589  fseqsupubi  12590  hashf1lem1  13044  wrddm  13109  swrdcl  13213  swrdnd2  13227  cats1un  13269  repswswrd  13324  limsupgle  13998  limsupgre  14002  rlim  14016  rlimi  14034  ello12  14037  lo1bdd  14041  elo12  14048  o1bdd  14052  lo1o1  14053  rlimclim  14067  rlimuni  14071  o1co  14107  rlimcn1  14109  isercolllem2  14186  isercolllem3  14187  fsumss  14245  fprodss  14459  ruclem11  14750  1arith  15411  vdwlem1  15465  vdwlem5  15469  vdwlem6  15470  vdwlem11  15475  ramval  15492  0ram  15504  0ram2  15505  0ramcl  15507  mrcuni  16046  homarcl2  16450  prfval  16604  intopsn  17018  gsumval  17036  gsumval2  17045  ghmrn  17438  ghmpreima  17447  cntzmhm2  17537  symgfixf1  17622  f1omvdconj  17631  pmtrfconj  17651  pmtrdifellem1  17661  pmtrdifellem2  17662  gsumval3lem1  18071  gsumval3lem2  18072  gsumval3  18073  gsumzres  18075  gsumzcl2  18076  gsumzf1o  18078  gsumzaddlem  18086  gsumzmhm  18102  gsumzoppg  18109  gsum2d  18136  dmdprdd  18163  dprdres  18192  dprdss  18193  dprdf1  18197  dmdprdsplitlem  18201  dprd2da  18206  dmdprdsplit2lem  18209  dmdprdsplit2  18210  dmdprdsplit  18211  dprdsplit  18212  dpjidcl  18222  ablfac1eulem  18236  ablfac1eu  18237  ablfaclem2  18250  ablfaclem3  18251  ablfac2  18253  lmhmpreima  18811  lmhmlsp  18812  mplcoe1  19228  mplcoe5  19231  psr1baslem  19318  gsumfsum  19574  evpmss  19692  regsumsupp  19728  pjdm2  19812  frlmlbs  19893  islindf2  19910  f1lindf  19918  islindf4  19934  mattpostpos  20017  mdetdiaglem  20161  decpmatval  20327  pmatcollpw3lem  20345  iinopn  20470  iscnp3  20796  lmbrf  20812  cnpnei  20816  cnclima  20820  iscncl  20821  cnntri  20823  cnclsi  20824  cncls2  20825  cncls  20826  cnntr  20827  cncnp  20832  cndis  20843  paste  20846  lmcnp  20856  cnt0  20898  cnt1  20902  cnhaus  20906  cncmp  20943  imacmp  20948  hauscmplem  20957  cnconn  20973  conima  20976  1stcfb  20996  1stccnp  21013  1stckgenlem  21104  kgencn  21107  kgencn3  21109  txcnpi  21159  txcnp  21171  txcnmpt  21175  prdstps  21180  xkohaus  21204  xkopt  21206  xkoco2cn  21209  xkococnlem  21210  qtopval2  21247  qtopcn  21265  qtopeu  21267  hmeores  21322  fbasrn  21436  fmval  21495  fmf  21497  rnelfmlem  21504  rnelfm  21505  fmfnfmlem2  21507  fmfnfmlem4  21509  fmfnfm  21510  cnflf2  21555  lmflf  21557  txflf  21558  cnextfval  21614  cnextcn  21619  clssubg  21660  ghmcnp  21666  tgphaus  21668  qustgplem  21672  tsmsval  21682  tsmsgsum  21690  ucncn  21837  psmetdmdm  21858  xmetdmdm  21887  metn0  21912  xmetres  21916  metres  21917  xmeter  21985  tmsval  22033  metcnp  22093  metustss  22103  metustid  22106  metustsym  22107  metustexhalf  22108  metustfbas  22109  cfilucfil  22111  metuel2  22117  restmetu  22122  isngp2  22148  evth  22493  lmmbrf  22782  iscfil2  22786  caufval  22795  iscau2  22797  iscauf  22800  caucfil  22803  equivcau  22820  lmclimf  22823  rrxcph  22901  rrxsuppss  22907  ovollb2  22977  ovolunlem1a  22984  ovoliunlem1  22990  ovoliun2  22994  ioombl1lem4  23049  uniioombllem1  23068  uniioombllem2  23070  uniioombllem6  23075  mbfconstlem  23115  ismbf  23116  ismbfcn  23117  mbfimaicc  23119  mbfmulc2lem  23133  mbfmulc2re  23134  mbfimaopn2  23143  cncombf  23144  mbfaddlem  23146  mbflimsup  23152  i1f0rn  23168  itg1addlem5  23186  itg1climres  23200  mbfmullem2  23210  ibl0  23272  cniccibl  23326  limcfval  23355  limcdif  23359  ellimc2  23360  ellimc3  23362  limccnp  23374  dvfval  23380  cpnord  23417  cpnres  23419  dvcmul  23426  dvcmulf  23427  dvnfre  23434  dvexp  23435  c1liplem1  23476  c1lip2  23478  dvgt0lem1  23482  dvcnvrelem1  23497  dvcnvrelem2  23498  mdegfval  23539  mdegleb  23541  mdegldg  23543  deg1mul3le  23593  plyco0  23665  plyeq0lem  23683  plyeq0  23684  plyaddlem1  23686  plymullem1  23687  dgrcl  23706  dgrub  23707  dgrlb  23709  plycpn  23761  vieta1lem1  23782  vieta1lem2  23783  aalioulem3  23806  taylfvallem1  23828  tayl0  23833  taylply2  23839  taylply  23840  dvtaylp  23841  dvntaylp  23842  dvntaylp0  23843  taylthlem1  23844  taylthlem2  23845  ulm2  23856  ulmss  23868  ulmdvlem1  23871  ulmdvlem2  23872  ulmdvlem3  23873  itgulm  23879  xrlimcnp  24408  basellem5  24524  dchrelbas2  24675  dchrghm  24694  dchrptlem1  24702  dchrptlem2  24703  iscgrgd  25122  iscgrglt  25123  trgcgrg  25124  tgcgr4  25140  motcgrg  25153  eedimeq  25492  axcontlem10  25567  uhgraun  25602  wrdumgra  25607  umgra1  25617  umgraun  25619  wlkn0  25817  eupares  26264  grporndm  26510  vcoprneOLD  26596  nvdm  26690  sspn  26775  dmadjrnb  27951  elnlfn  27973  xppreima  28631  fmptcof2  28641  curry2ima  28671  fpwrelmap  28698  smatrcl  28992  mdetpmtr1  29019  locfinreflem  29037  hauseqcn  29071  rge0scvg  29125  indpreima  29216  indf1ofs  29217  esumpcvgval  29269  ofcfval4  29296  isrnmeas  29392  measdivcst  29417  omsfval  29485  omscl  29486  omsf  29487  oms0  29488  omsmon  29489  omssubaddlem  29490  omssubadd  29491  carsgval  29494  carsggect  29509  omsmeas  29514  sibfof  29531  sitgclg  29533  eulerpartlemsv2  29549  eulerpartlemsf  29550  eulerpartlemv  29555  eulerpartlemd  29557  eulerpartlemb  29559  eulerpartlemt  29562  eulerpartlemr  29565  eulerpartlemgvv  29567  eulerpartlemgu  29568  eulerpartlemgs2  29571  eulerpartlemn  29572  sseqfv2  29585  rrvdm  29637  cvmliftmolem1  30319  cvmliftlem3  30325  cvmliftlem10  30332  cvmliftlem13  30334  cvmlift2lem9  30349  cvmlift3lem6  30362  cvmlift3lem7  30363  mrsubfval  30461  mclsax  30522  mclsppslem  30536  mclspps  30537  soseq  30797  nodmon  30849  fwddifval  31241  fwddifnval  31242  ivthALT  31302  bj-finsumval0  32123  curf  32356  uncf  32357  curunc  32360  unccur  32361  matunitlindflem2  32375  ptrecube  32378  heicant  32413  mbfresfi  32425  itg2addnclem  32430  itg2addnclem2  32431  cnicciblnc  32450  ftc1anclem1  32454  ftc1anclem5  32458  ftc1anclem6  32459  ftc1anclem8  32461  indexdom  32498  sdclem2  32507  cnres2  32531  sstotbnd2  32542  isbnd3  32552  ssbnd  32556  bnd2lem  32559  ismtyval  32568  ismgmOLD  32618  ismndo2  32642  exidreslem  32645  grpokerinj  32661  rngosn3  32692  rngodm1dm2  32700  divrngcl  32725  isdrngo2  32726  keridl  32800  ismrcd1  36078  istopclsd  36080  mapfzcons2  36099  coeq0i  36133  pw2f1ocnv  36421  fnwe2lem2  36438  lmhmfgima  36471  pwfi2f1o  36483  cnioobibld  36617  itgpowd  36618  wnefimgd  37279  funfvima2d  37290  binomcxplemnotnn0  37376  cncmpmax  38013  fresin2  38146  mapsnd  38182  fdmd  38214  evthiccabs  38365  mullimcf  38490  cncfuni  38572  cncficcgt0  38574  cncfioobd  38583  dvsinax  38601  dvsubcncf  38614  dvmulcncf  38615  dvdivcncf  38617  cnbdibl  38654  itgperiod  38673  fvvolioof  38682  fvvolicof  38684  stoweidlem29  38722  fourierdlem20  38820  fourierdlem48  38847  fourierdlem49  38848  fourierdlem53  38852  fourierdlem58  38857  fourierdlem59  38858  fourierdlem63  38862  fourierdlem68  38867  fourierdlem71  38870  fourierdlem73  38872  fourierdlem74  38873  fourierdlem75  38874  fourierdlem76  38875  fourierdlem80  38879  fourierdlem81  38880  fourierdlem82  38881  fourierdlem89  38888  fourierdlem91  38890  fourierdlem92  38891  fourierdlem93  38892  fourierdlem94  38893  fourierdlem111  38910  fourierdlem112  38911  fourierdlem113  38912  fouriercn  38925  sge0val  39059  fge0iccico  39063  sge0sn  39072  sge0tsms  39073  sge0cl  39074  sge0f1o  39075  sge0isum  39120  ismeannd  39160  isomennd  39221  hoicvr  39238  dmovn  39294  hspmbl  39319  ovolval4lem1  39339  ovnovollem1  39346  ovnovollem2  39347  fmtnoinf  39787  nnsum4primeseven  40017  nnsum4primesevenALTV  40018  uhgrun  40297  wrdupgr  40309  wrdumgr  40320  upgr1e  40336  upgrun  40341  umgrun  40343  1wlkn0  40823  1wlkres  40877  1wlkp1lem1  40880  pthdivtx  40933  domnmsuppn0  41942  rmsuppss  41943  mndpsuppss  41944  scmsuppss  41945  fdivmpt  42130  fdivmptf  42131  refdivmptf  42132  fdivpm  42133  refdivpm  42134  elbigo2  42142  elbigolo1  42147
  Copyright terms: Public domain W3C validator