Theorem fdm 5735

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

Syntax hints:   -> wi 4   = wceq 1379   dom cdm 4999   Fn wfn 5583   -->wf 5584

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 5591  df-f 5592

This theorem is referenced by:  fdmi  5736  fssxp  5743  ffdm  5745  f00  5767  f0dom0  5769  f0rn0  5770  foima  5800  foco  5805  resdif  5836  fimacnv  6013  dff3  6034  ffvresb  6052  fmptco  6054  dmfex  6742  fornex  6753  frnsuppeq  6913  suppss  6930  onnseq  7015  issmo2  7020  smoiso  7033  mapprc  7424  elpm2r  7436  map0b  7457  mapsn  7460  brdomg  7526  pw2f1olem  7621  fopwdom  7625  fodomfib  7800  fisuppfi  7837  intrnfi  7876  ordtypelem5  7947  ordtypelem6  7948  ordtypelem7  7949  ordtypelem8  7950  wemapso2OLD  7977  wemapso2lem  7978  brwdomn0  7995  wdomtr  8001  cantnfcl  8086  cantnfle  8090  cantnflt  8091  cantnff  8093  cantnfp1lem2  8098  cantnfp1lem3  8099  cantnflem1b  8105  cantnflem1d  8107  cantnflem1  8108  cantnflem3  8110  cantnfclOLD  8116  cantnfleOLD  8120  cantnfltOLD  8121  cantnfp1lem2OLD  8124  cantnfp1lem3OLD  8125  cantnflem1bOLD  8128  cantnflem1dOLD  8130  cantnflem1OLD  8131  cantnflem3OLD  8132  cnfcomlem  8143  cnfcom  8144  cnfcom2lem  8145  cnfcom3lem  8147  cnfcom3  8148  cnfcomlemOLD  8151  cnfcomOLD  8152  cnfcom2lemOLD  8153  cnfcom3lemOLD  8155  cnfcom3OLD  8156  iunmapdisj  8404  fseqenlem2  8406  fodomfi2  8441  infmap2  8598  coftr  8653  fin23lem30  8722  fin23lem40  8731  isf34lem5  8758  isf34lem7  8759  isf34lem6  8760  fin1a2lem7  8786  axdc3lem2  8831  axdc3lem4  8833  ttukeylem6  8894  fodomb  8904  pwxpndom2  9043  nn0suppOLD  10850  rpnnen1lem4  11211  rpnnen1lem5  11212  fseqsupcl  12055  fseqsupubi  12056  hashimarn  12462  hashfzdm  12464  hashfirdm  12466  hashf1lem1  12470  wrdsymb0  12540  lsw0  12551  swrdcl  12609  swrdval2  12610  swrdnd  12620  swrdvalodm2  12627  swrdvalodm  12628  cats1un  12664  repswswrd  12719  limsupgle  13263  limsupgre  13267  rlim  13281  rlimi  13299  ello12  13302  lo1bdd  13306  elo12  13313  o1bdd  13317  lo1o1  13318  rlimclim  13332  rlimuni  13336  lo1eq  13354  rlimeq  13355  rlimcld2  13364  o1co  13372  rlimcn1  13374  rlimcn2  13376  rlimsqzlem  13434  isercolllem2  13451  isercolllem3  13452  fsumss  13510  ruclem11  13834  1arith  14304  vdwlem1  14358  vdwlem5  14362  vdwlem6  14363  vdwlem11  14368  ramval  14385  0ram  14397  0ram2  14398  0ramcl  14400  mrcuni  14876  homarcl2  15220  prfval  15326  intopsn  15782  gsumval  15825  gsumval2  15835  ghmrn  16085  ghmpreima  16093  cntzmhm2  16182  symgfixf1  16268  f1omvdconj  16277  pmtrfconj  16297  pmtrdifellem1  16307  pmtrdifellem2  16308  gsumval3OLD  16711  gsumval3lem1  16712  gsumval3lem2  16713  gsumval3  16714  gsumzres  16717  gsumzcl2  16718  gsumzf1o  16720  gsumzresOLD  16721  gsumzclOLD  16722  gsumzf1oOLD  16723  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzmhm  16760  gsumzmhmOLD  16761  gsumzoppg  16770  gsumzoppgOLD  16771  gsum2d  16802  gsum2dOLD  16803  dmdprdd  16833  dprdres  16877  dprdss  16878  dprdz  16879  dprdf1  16882  dmdprdsplitlem  16886  dmdprdsplitlemOLD  16887  dprd2da  16893  dmdprdsplit2lem  16896  dmdprdsplit2  16897  dmdprdsplit  16898  dprdsplit  16899  dpjidcl  16909  dpjidclOLD  16916  ablfac1eulem  16925  ablfac1eu  16926  ablfaclem2  16939  ablfaclem3  16940  ablfac2  16942  lmhmpreima  17494  lmhmlsp  17495  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  psr1baslem  18023  gsumfsum  18280  evpmss  18417  regsumsupp  18453  pjdm2  18537  frlmlbs  18626  islindf2  18644  f1lindf  18652  islindf4  18668  mattpostpos  18751  mdetdiaglem  18895  decpmatval  19061  pmatcollpw3lem  19079  iinopn  19206  iscnp3  19539  lmbrf  19555  cnpnei  19559  cnclima  19563  iscncl  19564  cnntri  19566  cnclsi  19567  cncls2  19568  cncls  19569  cnntr  19570  cncnp  19575  cnrest  19580  cndis  19586  paste  19589  lmcnp  19599  cnt0  19641  cnt1  19645  cnhaus  19649  cncmp  19686  imacmp  19691  hauscmplem  19700  bwthOLD  19705  cnconn  19717  conima  19720  1stcfb  19740  1stccnp  19757  1stckgenlem  19817  kgencn  19820  kgencn3  19822  txcnpi  19872  txcnp  19884  txcnmpt  19888  prdstps  19893  xkohaus  19917  xkopt  19919  xkoco2cn  19922  xkococnlem  19923  qtopval2  19960  qtopcn  19978  qtopeu  19980  hmeores  20035  fbasrn  20148  fmval  20207  fmf  20209  rnelfmlem  20216  rnelfm  20217  fmfnfmlem2  20219  fmfnfmlem4  20221  fmfnfm  20222  cnflf2  20267  lmflf  20269  txflf  20270  alexsublem  20307  cnextfval  20325  cnextcn  20330  clssubg  20370  ghmcnp  20376  tgphaus  20378  divstgplem  20382  tsmsval  20392  tsmsgsum  20400  tsmsgsumOLD  20403  ucncn  20551  psmetdmdm  20572  xmetdmdm  20601  metn0  20626  xmetres  20630  metres  20631  xmeter  20699  tmsval  20747  metcnp  20807  metustssOLD  20819  metustss  20820  metustidOLD  20825  metustid  20826  metustsymOLD  20827  metustsym  20828  metustexhalfOLD  20829  metustexhalf  20830  metustfbasOLD  20831  metustfbas  20832  cfilucfilOLD  20835  cfilucfil  20836  metuel2  20845  restmetu  20853  isngp2  20880  evth  21222  lmmbrf  21464  iscfil2  21468  caufval  21477  iscau2  21479  iscauf  21482  caucfil  21485  cmetcaulem  21490  equivcau  21502  lmclimf  21505  rrxcph  21587  rrxsuppss  21593  minveclem3b  21606  ovollb2  21663  ovolunlem1a  21670  ovoliunlem1  21676  ovoliun2  21680  ioombl1lem4  21734  uniioombllem1  21753  uniioombllem2  21755  uniioombllem6  21760  mbfconstlem  21799  ismbf  21800  ismbfcn  21801  mbfimaicc  21803  mbfmulc2lem  21817  mbfmulc2re  21818  mbfneg  21820  mbfimaopn2  21827  cncombf  21828  mbfaddlem  21830  mbfsup  21834  mbfinf  21835  mbflimsup  21836  i1f0rn  21852  itg1addlem5  21870  itg1climres  21884  mbfmullem2  21894  itg2monolem1  21920  itg2mono  21923  itg2i1fseq2  21926  itg2cnlem1  21931  isibl2  21936  ibl0  21956  cniccibl  22010  limcfval  22039  limcdif  22043  ellimc2  22044  ellimc3  22046  limccnp  22058  limccnp2  22059  limcco  22060  dvfval  22064  cpnord  22101  cpnres  22103  dvcmul  22110  dvcmulf  22111  dvnfre  22118  dvexp  22119  c1liplem1  22160  c1lip2  22162  dvgt0lem1  22166  dvcnvrelem1  22181  dvcnvrelem2  22182  itgsubstlem  22212  mdegfval  22223  mdegleb  22227  mdegldg  22229  deg1mul3le  22280  plyco0  22352  plyeq0lem  22370  plyeq0  22371  plyaddlem1  22373  plymullem1  22374  dgrcl  22393  dgrub  22394  dgrlb  22396  plycpn  22447  vieta1lem1  22468  vieta1lem2  22469  aalioulem3  22492  taylfvallem1  22514  tayl0  22519  taylply2  22525  taylply  22526  dvtaylp  22527  dvntaylp  22528  dvntaylp0  22529  taylthlem1  22530  taylthlem2  22531  ulm2  22542  ulmss  22554  ulmdvlem1  22557  ulmdvlem2  22558  ulmdvlem3  22559  iblulm  22564  itgulm  22565  rlimcnp2  23052  xrlimcnp  23054  basellem5  23114  dchrelbas2  23268  dchrghm  23287  dchrptlem1  23295  dchrptlem2  23296  dchrisumlema  23429  iscgrgd  23661  trgcgrg  23662  motcgrg  23687  eedimeq  23905  axcontlem10  23980  uhgraun  24015  wrdumgra  24020  umgra1  24030  umgraun  24032  wlkn0  24231  eupares  24679  grporndm  24916  resgrprn  24986  isabloda  25005  subgores  25010  ismgm  25026  ismndo2  25051  ghsubgolem  25076  rngodm1dm2  25124  rngosn3  25132  vcoprne  25176  nvdm  25268  sspn  25353  htthlem  25538  dmadjrnb  26529  elnlfn  26551  xppreima  27187  fmptcof2  27202  curry2ima  27226  fpwrelmap  27256  hauseqcn  27541  rge0scvg  27595  indpreima  27706  indf1ofs  27707  esumpcvgval  27752  ofcfval4  27772  isrnmeas  27839  measdivcst  27864  omsfval  27933  oms0  27934  omsmon  27935  sibfof  27950  sitgclg  27952  eulerpartlemsv2  27965  eulerpartlemsf  27966  eulerpartlemv  27971  eulerpartlemd  27973  eulerpartlemb  27975  eulerpartlemt  27978  eulerpartlemr  27981  eulerpartlemgvv  27983  eulerpartlemgu  27984  eulerpartlemgs2  27987  eulerpartlemn  27988  sseqfv2  28001  rrvdm  28053  cvmliftmolem1  28394  cvmliftlem3  28400  cvmliftlem10  28407  cvmliftlem13  28409  cvmlift2lem9  28424  cvmlift3lem6  28437  cvmlift3lem7  28438  ghomfo  28534  fprodss  28685  soseq  28939  nodmon  29015  heicant  29654  mbfresfi  29666  itg2addnclem  29671  itg2addnclem2  29672  cnicciblnc  29691  ftc1anclem1  29695  ftc1anclem5  29699  ftc1anclem6  29700  ftc1anclem8  29702  ivthALT  29758  indexdom  29856  sdclem2  29866  cnres2  29890  sstotbnd2  29901  isbnd3  29911  ssbnd  29915  bnd2lem  29918  ismtyval  29927  exidreslem  29970  grpokerinj  29978  divrngcl  29991  isdrngo2  29992  keridl  30060  ismrcd1  30262  istopclsd  30264  mapfzcons2  30283  coeq0i  30318  pw2f1ocnv  30611  fnwe2lem2  30629  lmhmfgima  30662  fsuppeq  30675  pwfi2f1o  30676  cnioobibld  30814  itgpowd  30815  expgrowth  30868  cncmpmax  31013  fresin2  31054  evthiccabs  31121  mullimc  31186  mullimcf  31193  cncfuni  31253  cncficcgt0  31255  cncfioobd  31264  dvsinax  31269  dvsubcncf  31282  dvmulcncf  31283  dvdivcncf  31285  ditgeqiooicc  31306  cnbdibl  31308  itgperiod  31327  stoweidlem29  31357  dirkercncflem2  31432  fourierdlem20  31455  fourierdlem48  31483  fourierdlem49  31484  fourierdlem53  31488  fourierdlem58  31493  fourierdlem59  31494  fourierdlem63  31498  fourierdlem68  31503  fourierdlem71  31506  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem80  31515  fourierdlem81  31516  fourierdlem82  31517  fourierdlem89  31524  fourierdlem91  31526  fourierdlem92  31527  fourierdlem93  31528  fourierdlem94  31529  fourierdlem111  31546  fourierdlem112  31547  fourierdlem113  31548  fouriercn  31561  uhgun  31875  domnmsuppn0  32061  rmsuppss  32062  mndpsuppss  32063  scmsuppss  32064  bj-finsumval0  33753