Theorem fdm 5725

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 5721	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5670	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 16	1 |- ( F : A --> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1383   dom cdm 4989   Fn wfn 5573   -->wf 5574

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 5581  df-f 5582

This theorem is referenced by:  fdmi  5726  fssxp  5733  ffdm  5735  f00  5757  f0dom0  5759  f0rn0  5760  foima  5790  foco  5795  resdif  5826  fimacnv  6004  dff3  6029  ffvresb  6047  fmptco  6049  dmfex  6743  fornex  6754  frnsuppeq  6915  suppss  6932  onnseq  7017  issmo2  7022  smoiso  7035  mapprc  7426  elpm2r  7438  map0b  7459  mapsn  7462  brdomg  7528  pw2f1olem  7623  fopwdom  7627  fodomfib  7802  fisuppfi  7839  intrnfi  7878  ordtypelem5  7950  ordtypelem6  7951  ordtypelem7  7952  ordtypelem8  7953  wemapso2OLD  7980  wemapso2lem  7981  brwdomn0  7998  wdomtr  8004  cantnfcl  8089  cantnfle  8093  cantnflt  8094  cantnff  8096  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1d  8110  cantnflem1  8111  cantnflem3  8113  cantnfclOLD  8119  cantnfleOLD  8123  cantnfltOLD  8124  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnflem3OLD  8135  cnfcomlem  8146  cnfcom  8147  cnfcom2lem  8148  cnfcom3lem  8150  cnfcom3  8151  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom2lemOLD  8156  cnfcom3lemOLD  8158  cnfcom3OLD  8159  iunmapdisj  8407  fseqenlem2  8409  fodomfi2  8444  infmap2  8601  coftr  8656  fin23lem30  8725  fin23lem40  8734  isf34lem5  8761  isf34lem7  8762  isf34lem6  8763  fin1a2lem7  8789  axdc3lem2  8834  axdc3lem4  8836  ttukeylem6  8897  fodomb  8907  pwxpndom2  9046  nn0suppOLD  10856  rpnnen1lem4  11220  rpnnen1lem5  11221  fseqsupcl  12066  fseqsupubi  12067  hashimarn  12475  hashfzdm  12477  hashfirdm  12479  hashf1lem1  12483  wrdsymb0  12554  lsw0  12565  swrdcl  12625  swrdval2  12626  swrdnd  12636  swrdvalodm2  12643  swrdvalodm  12644  cats1un  12680  repswswrd  12735  limsupgle  13279  limsupgre  13283  rlim  13297  rlimi  13315  ello12  13318  lo1bdd  13322  elo12  13329  o1bdd  13333  lo1o1  13334  rlimclim  13348  rlimuni  13352  o1co  13388  rlimcn1  13390  isercolllem2  13467  isercolllem3  13468  fsumss  13526  ruclem11  13850  1arith  14322  vdwlem1  14376  vdwlem5  14380  vdwlem6  14381  vdwlem11  14386  ramval  14403  0ram  14415  0ram2  14416  0ramcl  14418  mrcuni  14895  homarcl2  15236  prfval  15342  intopsn  15756  gsumval  15772  gsumval2  15781  ghmrn  16154  ghmpreima  16162  cntzmhm2  16251  symgfixf1  16336  f1omvdconj  16345  pmtrfconj  16365  pmtrdifellem1  16375  pmtrdifellem2  16376  gsumval3OLD  16782  gsumval3lem1  16783  gsumval3lem2  16784  gsumval3  16785  gsumzres  16788  gsumzcl2  16789  gsumzf1o  16791  gsumzresOLD  16792  gsumzclOLD  16793  gsumzf1oOLD  16794  gsumzaddlem  16808  gsumzaddlemOLD  16810  gsumzmhm  16831  gsumzmhmOLD  16832  gsumzoppg  16841  gsumzoppgOLD  16842  gsum2d  16873  gsum2dOLD  16874  dmdprdd  16904  dprdres  16949  dprdss  16950  dprdf1  16954  dmdprdsplitlem  16958  dmdprdsplitlemOLD  16959  dprd2da  16965  dmdprdsplit2lem  16968  dmdprdsplit2  16969  dmdprdsplit  16970  dprdsplit  16971  dpjidcl  16981  dpjidclOLD  16988  ablfac1eulem  16997  ablfac1eu  16998  ablfaclem2  17011  ablfaclem3  17012  ablfac2  17014  lmhmpreima  17568  lmhmlsp  17569  mplcoe1  18001  mplcoe5  18005  mplcoe2OLD  18007  psr1baslem  18098  gsumfsum  18358  evpmss  18495  regsumsupp  18531  pjdm2  18615  frlmlbs  18704  islindf2  18722  f1lindf  18730  islindf4  18746  mattpostpos  18829  mdetdiaglem  18973  decpmatval  19139  pmatcollpw3lem  19157  iinopn  19284  iscnp3  19618  lmbrf  19634  cnpnei  19638  cnclima  19642  iscncl  19643  cnntri  19645  cnclsi  19646  cncls2  19647  cncls  19648  cnntr  19649  cncnp  19654  cndis  19665  paste  19668  lmcnp  19678  cnt0  19720  cnt1  19724  cnhaus  19728  cncmp  19765  imacmp  19770  hauscmplem  19779  bwthOLD  19784  cnconn  19796  conima  19799  1stcfb  19819  1stccnp  19836  1stckgenlem  19927  kgencn  19930  kgencn3  19932  txcnpi  19982  txcnp  19994  txcnmpt  19998  prdstps  20003  xkohaus  20027  xkopt  20029  xkoco2cn  20032  xkococnlem  20033  qtopval2  20070  qtopcn  20088  qtopeu  20090  hmeores  20145  fbasrn  20258  fmval  20317  fmf  20319  rnelfmlem  20326  rnelfm  20327  fmfnfmlem2  20329  fmfnfmlem4  20331  fmfnfm  20332  cnflf2  20377  lmflf  20379  txflf  20380  cnextfval  20435  cnextcn  20440  clssubg  20480  ghmcnp  20486  tgphaus  20488  qustgplem  20492  tsmsval  20502  tsmsgsum  20510  tsmsgsumOLD  20513  ucncn  20661  psmetdmdm  20682  xmetdmdm  20711  metn0  20736  xmetres  20740  metres  20741  xmeter  20809  tmsval  20857  metcnp  20917  metustssOLD  20929  metustss  20930  metustidOLD  20935  metustid  20936  metustsymOLD  20937  metustsym  20938  metustexhalfOLD  20939  metustexhalf  20940  metustfbasOLD  20941  metustfbas  20942  cfilucfilOLD  20945  cfilucfil  20946  metuel2  20955  restmetu  20963  isngp2  20990  evth  21332  lmmbrf  21574  iscfil2  21578  caufval  21587  iscau2  21589  iscauf  21592  caucfil  21595  equivcau  21612  lmclimf  21615  rrxcph  21697  rrxsuppss  21703  ovollb2  21773  ovolunlem1a  21780  ovoliunlem1  21786  ovoliun2  21790  ioombl1lem4  21844  uniioombllem1  21863  uniioombllem2  21865  uniioombllem6  21870  mbfconstlem  21909  ismbf  21910  ismbfcn  21911  mbfimaicc  21913  mbfmulc2lem  21927  mbfmulc2re  21928  mbfimaopn2  21937  cncombf  21938  mbfaddlem  21940  mbflimsup  21946  i1f0rn  21962  itg1addlem5  21980  itg1climres  21994  mbfmullem2  22004  ibl0  22066  cniccibl  22120  limcfval  22149  limcdif  22153  ellimc2  22154  ellimc3  22156  limccnp  22168  dvfval  22174  cpnord  22211  cpnres  22213  dvcmul  22220  dvcmulf  22221  dvnfre  22228  dvexp  22229  c1liplem1  22270  c1lip2  22272  dvgt0lem1  22276  dvcnvrelem1  22291  dvcnvrelem2  22292  mdegfval  22333  mdegleb  22337  mdegldg  22339  deg1mul3le  22390  plyco0  22462  plyeq0lem  22480  plyeq0  22481  plyaddlem1  22483  plymullem1  22484  dgrcl  22503  dgrub  22504  dgrlb  22506  plycpn  22557  vieta1lem1  22578  vieta1lem2  22579  aalioulem3  22602  taylfvallem1  22624  tayl0  22629  taylply2  22635  taylply  22636  dvtaylp  22637  dvntaylp  22638  dvntaylp0  22639  taylthlem1  22640  taylthlem2  22641  ulm2  22652  ulmss  22664  ulmdvlem1  22667  ulmdvlem2  22668  ulmdvlem3  22669  itgulm  22675  xrlimcnp  23170  basellem5  23230  dchrelbas2  23384  dchrghm  23403  dchrptlem1  23411  dchrptlem2  23412  iscgrgd  23777  trgcgrg  23778  motcgrg  23803  eedimeq  24073  axcontlem10  24148  uhgraun  24183  wrdumgra  24188  umgra1  24198  umgraun  24200  wlkn0  24399  eupares  24847  grporndm  25084  resgrprn  25154  isabloda  25173  subgores  25178  ismgmOLD  25194  ismndo2  25219  ghsubgolemOLD  25244  rngodm1dm2  25292  rngosn3  25300  vcoprne  25344  nvdm  25436  sspn  25521  dmadjrnb  26697  elnlfn  26719  xppreima  27359  fmptcof2  27374  curry2ima  27398  fpwrelmap  27428  locfinreflem  27716  hauseqcn  27750  rge0scvg  27804  indpreima  27911  indf1ofs  27912  esumpcvgval  27957  ofcfval4  27977  isrnmeas  28044  measdivcst  28069  omsfval  28138  oms0  28139  omsmon  28140  sibfof  28155  sitgclg  28157  eulerpartlemsv2  28170  eulerpartlemsf  28171  eulerpartlemv  28176  eulerpartlemd  28178  eulerpartlemb  28180  eulerpartlemt  28183  eulerpartlemr  28186  eulerpartlemgvv  28188  eulerpartlemgu  28189  eulerpartlemgs2  28192  eulerpartlemn  28193  sseqfv2  28206  rrvdm  28258  cvmliftmolem1  28599  cvmliftlem3  28605  cvmliftlem10  28612  cvmliftlem13  28614  cvmlift2lem9  28629  cvmlift3lem6  28642  cvmlift3lem7  28643  mrsubfval  28741  mclsax  28802  mclsppslem  28816  mclspps  28817  ghomfo  28904  fprodss  29055  soseq  29309  nodmon  29385  heicant  30024  mbfresfi  30036  itg2addnclem  30041  itg2addnclem2  30042  cnicciblnc  30061  ftc1anclem1  30065  ftc1anclem5  30069  ftc1anclem6  30070  ftc1anclem8  30072  ivthALT  30128  indexdom  30200  sdclem2  30210  cnres2  30234  sstotbnd2  30245  isbnd3  30255  ssbnd  30259  bnd2lem  30262  ismtyval  30271  exidreslem  30314  grpokerinj  30322  divrngcl  30335  isdrngo2  30336  keridl  30404  ismrcd1  30605  istopclsd  30607  mapfzcons2  30626  coeq0i  30661  pw2f1ocnv  30954  fnwe2lem2  30972  lmhmfgima  31005  fsuppeq  31018  pwfi2f1o  31019  cnioobibld  31157  itgpowd  31158  cncmpmax  31361  fresin2  31398  evthiccabs  31465  mullimcf  31537  cncfuni  31596  cncficcgt0  31598  cncfioobd  31607  dvsinax  31612  dvsubcncf  31625  dvmulcncf  31626  dvdivcncf  31628  cnbdibl  31651  itgperiod  31670  stoweidlem29  31700  fourierdlem20  31798  fourierdlem48  31826  fourierdlem49  31827  fourierdlem53  31831  fourierdlem58  31836  fourierdlem59  31837  fourierdlem63  31841  fourierdlem68  31846  fourierdlem71  31849  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem80  31858  fourierdlem81  31859  fourierdlem82  31860  fourierdlem89  31867  fourierdlem91  31869  fourierdlem92  31870  fourierdlem93  31871  fourierdlem94  31872  fourierdlem111  31889  fourierdlem112  31890  fourierdlem113  31891  fouriercn  31904  uhgun  32218  domnmsuppn0  32697  rmsuppss  32698  mndpsuppss  32699  scmsuppss  32700  bj-finsumval0  34403  wnefimgd  37643  funfvima2d  37655