Theorem fdm 5643

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

Step	Hyp	Ref	Expression
1		ffn 5639	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5588	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 16	1 |- ( F : A --> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1399   dom cdm 4913   Fn wfn 5491   -->wf 5492

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 369  df-fn 5499  df-f 5500

This theorem is referenced by:  fdmi  5644  fssxp  5651  ffdm  5653  f00  5675  f0dom0  5677  f0rn0  5678  foima  5708  foco  5713  resdif  5744  fimacnv  5921  dff3  5946  ffvresb  5964  fmptco  5966  dmfex  6657  fornex  6668  frnsuppeq  6829  suppss  6848  onnseq  6933  issmo2  6938  smoiso  6951  mapprc  7342  elpm2r  7355  map0b  7376  mapsn  7379  brdomg  7445  pw2f1olem  7540  fopwdom  7544  fodomfib  7715  fisuppfi  7752  intrnfi  7791  ordtypelem5  7862  ordtypelem6  7863  ordtypelem7  7864  ordtypelem8  7865  wemapso2OLD  7892  wemapso2lem  7893  brwdomn0  7910  wdomtr  7916  cantnfcl  7999  cantnfle  8003  cantnflt  8004  cantnff  8006  cantnfp1lem3  8012  cantnflem1b  8018  cantnflem1d  8020  cantnflem1  8021  cantnflem3  8023  cantnfclOLD  8029  cantnfleOLD  8033  cantnfltOLD  8034  cantnfp1lem2OLD  8037  cantnfp1lem3OLD  8038  cantnflem1bOLD  8041  cantnflem1dOLD  8043  cantnflem1OLD  8044  cantnflem3OLD  8045  cnfcomlem  8056  cnfcom  8057  cnfcom2lem  8058  cnfcom3lem  8060  cnfcom3  8061  cnfcomlemOLD  8064  cnfcomOLD  8065  cnfcom2lemOLD  8066  cnfcom3lemOLD  8068  cnfcom3OLD  8069  iunmapdisj  8317  fseqenlem2  8319  fodomfi2  8354  infmap2  8511  coftr  8566  fin23lem30  8635  fin23lem40  8644  isf34lem5  8671  isf34lem7  8672  isf34lem6  8673  fin1a2lem7  8699  axdc3lem2  8744  axdc3lem4  8746  ttukeylem6  8807  fodomb  8817  pwxpndom2  8954  nn0suppOLD  10767  rpnnen1lem4  11130  rpnnen1lem5  11131  fseqsupcl  11990  fseqsupubi  11991  hashimarn  12400  hashfzdm  12402  hashfirdm  12404  hashf1lem1  12408  wrddm  12460  swrdcl  12555  swrdnd2  12569  cats1un  12612  repswswrd  12667  limsupgle  13302  limsupgre  13306  rlim  13320  rlimi  13338  ello12  13341  lo1bdd  13345  elo12  13352  o1bdd  13356  lo1o1  13357  rlimclim  13371  rlimuni  13375  o1co  13411  rlimcn1  13413  isercolllem2  13490  isercolllem3  13491  fsumss  13549  fprodss  13757  ruclem11  13975  1arith  14447  vdwlem1  14501  vdwlem5  14505  vdwlem6  14506  vdwlem11  14511  ramval  14528  0ram  14540  0ram2  14541  0ramcl  14543  mrcuni  15028  homarcl2  15431  prfval  15585  intopsn  15999  gsumval  16015  gsumval2  16024  ghmrn  16397  ghmpreima  16405  cntzmhm2  16494  symgfixf1  16579  f1omvdconj  16588  pmtrfconj  16608  pmtrdifellem1  16618  pmtrdifellem2  16619  gsumval3OLD  17025  gsumval3lem1  17026  gsumval3lem2  17027  gsumval3  17028  gsumzres  17031  gsumzcl2  17032  gsumzf1o  17034  gsumzresOLD  17035  gsumzclOLD  17036  gsumzf1oOLD  17037  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsumzmhm  17073  gsumzmhmOLD  17074  gsumzoppg  17083  gsumzoppgOLD  17084  gsum2d  17113  gsum2dOLD  17114  dmdprdd  17143  dprdres  17188  dprdss  17189  dprdf1  17193  dmdprdsplitlem  17197  dmdprdsplitlemOLD  17198  dprd2da  17204  dmdprdsplit2lem  17207  dmdprdsplit2  17208  dmdprdsplit  17209  dprdsplit  17210  dpjidcl  17220  dpjidclOLD  17227  ablfac1eulem  17236  ablfac1eu  17237  ablfaclem2  17250  ablfaclem3  17251  ablfac2  17253  lmhmpreima  17807  lmhmlsp  17808  mplcoe1  18240  mplcoe5  18244  mplcoe2OLD  18246  psr1baslem  18337  gsumfsum  18597  evpmss  18713  regsumsupp  18749  pjdm2  18833  frlmlbs  18917  islindf2  18934  f1lindf  18942  islindf4  18958  mattpostpos  19041  mdetdiaglem  19185  decpmatval  19351  pmatcollpw3lem  19369  iinopn  19496  iscnp3  19831  lmbrf  19847  cnpnei  19851  cnclima  19855  iscncl  19856  cnntri  19858  cnclsi  19859  cncls2  19860  cncls  19861  cnntr  19862  cncnp  19867  cndis  19878  paste  19881  lmcnp  19891  cnt0  19933  cnt1  19937  cnhaus  19941  cncmp  19978  imacmp  19983  hauscmplem  19992  cnconn  20008  conima  20011  1stcfb  20031  1stccnp  20048  1stckgenlem  20139  kgencn  20142  kgencn3  20144  txcnpi  20194  txcnp  20206  txcnmpt  20210  prdstps  20215  xkohaus  20239  xkopt  20241  xkoco2cn  20244  xkococnlem  20245  qtopval2  20282  qtopcn  20300  qtopeu  20302  hmeores  20357  fbasrn  20470  fmval  20529  fmf  20531  rnelfmlem  20538  rnelfm  20539  fmfnfmlem2  20541  fmfnfmlem4  20543  fmfnfm  20544  cnflf2  20589  lmflf  20591  txflf  20592  cnextfval  20647  cnextcn  20652  clssubg  20692  ghmcnp  20698  tgphaus  20700  qustgplem  20704  tsmsval  20714  tsmsgsum  20722  tsmsgsumOLD  20725  ucncn  20873  psmetdmdm  20894  xmetdmdm  20923  metn0  20948  xmetres  20952  metres  20953  xmeter  21021  tmsval  21069  metcnp  21129  metustssOLD  21141  metustss  21142  metustidOLD  21147  metustid  21148  metustsymOLD  21149  metustsym  21150  metustexhalfOLD  21151  metustexhalf  21152  metustfbasOLD  21153  metustfbas  21154  cfilucfilOLD  21157  cfilucfil  21158  metuel2  21167  restmetu  21175  isngp2  21202  evth  21544  lmmbrf  21786  iscfil2  21790  caufval  21799  iscau2  21801  iscauf  21804  caucfil  21807  equivcau  21824  lmclimf  21827  rrxcph  21909  rrxsuppss  21915  ovollb2  21985  ovolunlem1a  21992  ovoliunlem1  21998  ovoliun2  22002  ioombl1lem4  22056  uniioombllem1  22075  uniioombllem2  22077  uniioombllem6  22082  mbfconstlem  22121  ismbf  22122  ismbfcn  22123  mbfimaicc  22125  mbfmulc2lem  22139  mbfmulc2re  22140  mbfimaopn2  22149  cncombf  22150  mbfaddlem  22152  mbflimsup  22158  i1f0rn  22174  itg1addlem5  22192  itg1climres  22206  mbfmullem2  22216  ibl0  22278  cniccibl  22332  limcfval  22361  limcdif  22365  ellimc2  22366  ellimc3  22368  limccnp  22380  dvfval  22386  cpnord  22423  cpnres  22425  dvcmul  22432  dvcmulf  22433  dvnfre  22440  dvexp  22441  c1liplem1  22482  c1lip2  22484  dvgt0lem1  22488  dvcnvrelem1  22503  dvcnvrelem2  22504  mdegfval  22545  mdegleb  22549  mdegldg  22551  deg1mul3le  22602  plyco0  22674  plyeq0lem  22692  plyeq0  22693  plyaddlem1  22695  plymullem1  22696  dgrcl  22715  dgrub  22716  dgrlb  22718  plycpn  22770  vieta1lem1  22791  vieta1lem2  22792  aalioulem3  22815  taylfvallem1  22837  tayl0  22842  taylply2  22848  taylply  22849  dvtaylp  22850  dvntaylp  22851  dvntaylp0  22852  taylthlem1  22853  taylthlem2  22854  ulm2  22865  ulmss  22877  ulmdvlem1  22880  ulmdvlem2  22881  ulmdvlem3  22882  itgulm  22888  xrlimcnp  23415  basellem5  23475  dchrelbas2  23629  dchrghm  23648  dchrptlem1  23656  dchrptlem2  23657  iscgrgd  24025  trgcgrg  24026  motcgrg  24051  eedimeq  24322  axcontlem10  24397  uhgraun  24432  wrdumgra  24437  umgra1  24447  umgraun  24449  wlkn0  24648  eupares  25096  grporndm  25329  resgrprn  25399  isabloda  25418  subgores  25423  ismgmOLD  25439  ismndo2  25464  ghsubgolemOLD  25489  rngodm1dm2  25537  rngosn3  25545  vcoprne  25589  nvdm  25681  sspn  25766  dmadjrnb  26941  elnlfn  26963  xppreima  27627  fmptcof2  27643  curry2ima  27674  fpwrelmap  27706  locfinreflem  27997  hauseqcn  28031  rge0scvg  28085  indpreima  28173  indf1ofs  28174  esumpcvgval  28226  ofcfval4  28253  isrnmeas  28327  measdivcst  28352  omsfval  28421  omscl  28422  omsf  28423  oms0  28424  omsmon  28425  omssubaddlem  28426  omssubadd  28427  carsgval  28430  carsggect  28445  omsmeas  28450  sibfof  28465  sitgclg  28467  eulerpartlemsv2  28480  eulerpartlemsf  28481  eulerpartlemv  28486  eulerpartlemd  28488  eulerpartlemb  28490  eulerpartlemt  28493  eulerpartlemr  28496  eulerpartlemgvv  28498  eulerpartlemgu  28499  eulerpartlemgs2  28502  eulerpartlemn  28503  sseqfv2  28516  rrvdm  28568  cvmliftmolem1  28915  cvmliftlem3  28921  cvmliftlem10  28928  cvmliftlem13  28930  cvmlift2lem9  28945  cvmlift3lem6  28958  cvmlift3lem7  28959  mrsubfval  29057  mclsax  29118  mclsppslem  29132  mclspps  29133  ghomfo  29220  soseq  29499  nodmon  29575  heicant  30214  mbfresfi  30226  itg2addnclem  30232  itg2addnclem2  30233  cnicciblnc  30252  ftc1anclem1  30256  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem8  30263  ivthALT  30319  indexdom  30391  sdclem2  30401  cnres2  30425  sstotbnd2  30436  isbnd3  30446  ssbnd  30450  bnd2lem  30453  ismtyval  30462  exidreslem  30505  grpokerinj  30513  divrngcl  30526  isdrngo2  30527  keridl  30595  ismrcd1  30796  istopclsd  30798  mapfzcons2  30817  coeq0i  30851  pw2f1ocnv  31145  fnwe2lem2  31163  lmhmfgima  31196  fsuppeq  31209  pwfi2f1o  31210  pwfi2f1oOLD  31211  cnioobibld  31349  itgpowd  31350  binomcxplemnotnn0  31429  cncmpmax  31574  fresin2  31615  evthiccabs  31695  mullimcf  31795  cncfuni  31855  cncficcgt0  31857  cncfioobd  31866  dvsinax  31874  dvsubcncf  31887  dvmulcncf  31888  dvdivcncf  31890  cnbdibl  31927  itgperiod  31946  stoweidlem29  31977  fourierdlem20  32075  fourierdlem48  32103  fourierdlem49  32104  fourierdlem53  32108  fourierdlem58  32113  fourierdlem59  32114  fourierdlem63  32118  fourierdlem68  32123  fourierdlem71  32126  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem76  32131  fourierdlem80  32135  fourierdlem81  32136  fourierdlem82  32137  fourierdlem89  32144  fourierdlem91  32146  fourierdlem92  32147  fourierdlem93  32148  fourierdlem94  32149  fourierdlem111  32166  fourierdlem112  32167  fourierdlem113  32168  fouriercn  32181  uhgun  32698  domnmsuppn0  33162  rmsuppss  33163  mndpsuppss  33164  scmsuppss  33165  fdivmpt  33361  fdivmptf  33362  refdivmptf  33363  fdivpm  33364  refdivpm  33365  elbigo2  33373  elbigolo1  33378  bj-finsumval0  35010  wnefimgd  38503  funfvima2d  38515