Theorem fdm 5551

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

Syntax hints:   -> wi 4   = wceq 1362   dom cdm 4827   Fn wfn 5401   -->wf 5402

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 5409  df-f 5410

This theorem is referenced by:  fdmi  5552  fssxp  5558  ffdm  5560  f00  5581  f0dom0  5583  foima  5613  foco  5618  resdif  5649  fimacnv  5823  dff3  5844  ffvresb  5861  fmptco  5863  dmfex  6524  fornex  6535  frnsuppeq  6691  suppss  6708  onnseq  6791  issmo2  6796  smoiso  6809  mapprc  7206  elpm2r  7218  map0b  7239  mapsn  7242  brdomg  7308  pw2f1olem  7403  fopwdom  7407  fodomfib  7579  fisuppfi  7616  intrnfi  7654  ordtypelem5  7724  ordtypelem6  7725  ordtypelem7  7726  ordtypelem8  7727  wemapso2OLD  7754  wemapso2lem  7755  brwdomn0  7772  wdomtr  7778  cantnfcl  7863  cantnfle  7867  cantnflt  7868  cantnff  7870  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1d  7884  cantnflem1  7885  cantnflem3  7887  cantnfclOLD  7893  cantnfleOLD  7897  cantnfltOLD  7898  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnflem3OLD  7909  cnfcomlem  7920  cnfcom  7921  cnfcom2lem  7922  cnfcom3lem  7924  cnfcom3  7925  cnfcomlemOLD  7928  cnfcomOLD  7929  cnfcom2lemOLD  7930  cnfcom3lemOLD  7932  cnfcom3OLD  7933  iunmapdisj  8181  fseqenlem2  8183  fodomfi2  8218  infmap2  8375  coftr  8430  fin23lem30  8499  fin23lem40  8508  isf34lem5  8535  isf34lem7  8536  isf34lem6  8537  fin1a2lem7  8563  axdc3lem2  8608  axdc3lem4  8610  ttukeylem6  8671  fodomb  8681  pwxpndom2  8819  nn0suppOLD  10621  rpnnen1lem4  10969  rpnnen1lem5  10970  fseqsupcl  11782  fseqsupubi  11783  hashimarn  12183  hashfzdm  12185  hashfirdm  12187  hashf1lem1  12191  wrdsymb0  12242  lsw0  12250  swrdcl  12298  swrdval2  12299  swrdnd  12309  swrdvalodm2  12316  swrdvalodm  12317  cats1un  12353  repswswrd  12405  limsupgle  12938  limsupgre  12942  rlim  12956  rlimi  12974  ello12  12977  lo1bdd  12981  elo12  12988  o1bdd  12992  lo1o1  12993  rlimclim  13007  rlimuni  13011  lo1eq  13029  rlimeq  13030  rlimcld2  13039  o1co  13047  rlimcn1  13049  rlimcn2  13051  rlimsqzlem  13109  isercolllem2  13126  isercolllem3  13127  fsumss  13185  ruclem11  13504  1arith  13970  vdwlem1  14024  vdwlem5  14028  vdwlem6  14029  vdwlem11  14034  ramval  14051  0ram  14063  0ram2  14064  0ramcl  14066  mrcuni  14541  homarcl2  14885  prfval  14991  gsumval  15484  gsumval2  15492  ghmrn  15739  ghmpreima  15747  cntzmhm2  15836  symgfixf1  15922  f1omvdconj  15931  pmtrfconj  15951  pmtrdifellem1  15961  pmtrdifellem2  15962  gsumval3OLD  16361  gsumval3lem1  16362  gsumval3lem2  16363  gsumval3  16364  gsumzres  16367  gsumzcl2  16368  gsumzf1o  16370  gsumzresOLD  16371  gsumzclOLD  16372  gsumzf1oOLD  16373  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumzmhm  16406  gsumzmhmOLD  16407  gsumzoppg  16415  gsumzoppgOLD  16416  gsum2d  16436  gsum2dOLD  16437  dmdprdd  16454  dprdres  16498  dprdss  16499  dprdz  16500  dprdf1  16503  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  dprd2da  16514  dmdprdsplit2lem  16517  dmdprdsplit2  16518  dmdprdsplit  16519  dprdsplit  16520  dpjidcl  16530  dpjidclOLD  16537  ablfac1eulem  16546  ablfac1eu  16547  ablfaclem2  16560  ablfaclem3  16561  ablfac2  16563  lmhmpreima  17050  lmhmlsp  17051  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  psr1baslem  17539  gsumfsum  17722  evpmss  17857  regsumsupp  17893  pjdm2  17977  frlmlbs  18066  islindf2  18084  f1lindf  18092  islindf4  18108  mattpostpos  18179  mdet1  18249  iinopn  18356  iscnp3  18689  lmbrf  18705  cnpnei  18709  cnclima  18713  iscncl  18714  cnntri  18716  cnclsi  18717  cncls2  18718  cncls  18719  cnntr  18720  cncnp  18725  cnrest  18730  cndis  18736  paste  18739  lmcnp  18749  cnt0  18791  cnt1  18795  cnhaus  18799  cncmp  18836  imacmp  18841  hauscmplem  18850  bwthOLD  18855  cnconn  18867  conima  18870  1stcfb  18890  1stccnp  18907  1stckgenlem  18967  kgencn  18970  kgencn3  18972  txcnpi  19022  txcnp  19034  txcnmpt  19038  prdstps  19043  xkohaus  19067  xkopt  19069  xkoco2cn  19072  xkococnlem  19073  qtopval2  19110  qtopcn  19128  qtopeu  19130  hmeores  19185  fbasrn  19298  fmval  19357  fmf  19359  rnelfmlem  19366  rnelfm  19367  fmfnfmlem2  19369  fmfnfmlem4  19371  fmfnfm  19372  cnflf2  19417  lmflf  19419  txflf  19420  alexsublem  19457  cnextfval  19475  cnextcn  19480  clssubg  19520  ghmcnp  19526  tgphaus  19528  divstgplem  19532  tsmsval  19542  tsmsgsum  19550  tsmsgsumOLD  19553  ucncn  19701  psmetdmdm  19722  xmetdmdm  19751  metn0  19776  xmetres  19780  metres  19781  xmeter  19849  tmsval  19897  metcnp  19957  metustssOLD  19969  metustss  19970  metustidOLD  19975  metustid  19976  metustsymOLD  19977  metustsym  19978  metustexhalfOLD  19979  metustexhalf  19980  metustfbasOLD  19981  metustfbas  19982  cfilucfilOLD  19985  cfilucfil  19986  metuel2  19995  restmetu  20003  isngp2  20030  evth  20372  lmmbrf  20614  iscfil2  20618  caufval  20627  iscau2  20629  iscauf  20632  caucfil  20635  cmetcaulem  20640  equivcau  20652  lmclimf  20655  rrxcph  20737  rrxsuppss  20743  minveclem3b  20756  ovollb2  20813  ovolunlem1a  20820  ovoliunlem1  20826  ovoliun2  20830  ioombl1lem4  20883  uniioombllem1  20902  uniioombllem2  20904  uniioombllem6  20909  mbfconstlem  20948  ismbf  20949  ismbfcn  20950  mbfimaicc  20952  mbfmulc2lem  20966  mbfmulc2re  20967  mbfneg  20969  mbfimaopn2  20976  cncombf  20977  mbfaddlem  20979  mbfsup  20983  mbfinf  20984  mbflimsup  20985  i1f0rn  21001  itg1addlem5  21019  itg1climres  21033  mbfmullem2  21043  itg2monolem1  21069  itg2mono  21072  itg2i1fseq2  21075  itg2cnlem1  21080  isibl2  21085  ibl0  21105  cniccibl  21159  limcfval  21188  limcdif  21192  ellimc2  21193  ellimc3  21195  limccnp  21207  limccnp2  21208  limcco  21209  dvfval  21213  cpnord  21250  cpnres  21252  dvcmul  21259  dvcmulf  21260  dvnfre  21267  dvexp  21268  c1liplem1  21309  c1lip2  21311  dvgt0lem1  21315  dvcnvrelem1  21330  dvcnvrelem2  21331  itgsubstlem  21361  mdegfval  21415  mdegleb  21419  mdegldg  21421  deg1mul3le  21472  plyco0  21544  plyeq0lem  21562  plyeq0  21563  plyaddlem1  21565  plymullem1  21566  dgrcl  21585  dgrub  21586  dgrlb  21588  plycpn  21639  vieta1lem1  21660  vieta1lem2  21661  aalioulem3  21684  taylfvallem1  21706  tayl0  21711  taylply2  21717  taylply  21718  dvtaylp  21719  dvntaylp  21720  dvntaylp0  21721  taylthlem1  21722  taylthlem2  21723  ulm2  21734  ulmss  21746  ulmdvlem1  21749  ulmdvlem2  21750  ulmdvlem3  21751  iblulm  21756  itgulm  21757  rlimcnp2  22244  xrlimcnp  22246  basellem5  22306  dchrelbas2  22460  dchrghm  22479  dchrptlem1  22487  dchrptlem2  22488  dchrisumlema  22621  iscgrgd  22846  trgcgrg  22847  eedimeq  22966  axcontlem10  23041  uhgraun  23067  wrdumgra  23072  umgra1  23082  umgraun  23084  eupares  23418  grporndm  23519  resgrprn  23589  isabloda  23608  subgores  23613  ismgm  23629  ismndo2  23654  ghsubgolem  23679  rngodm1dm2  23727  rngosn3  23735  vcoprne  23779  nvdm  23871  sspn  23956  htthlem  24141  dmadjrnb  25132  elnlfn  25154  xppreima  25787  fmptcof2  25802  curry2ima  25826  nn0supp  25851  ffs2  25852  fpwrelmap  25857  hauseqcn  26178  rge0scvg  26232  indpreima  26334  indf1ofs  26335  esumpcvgval  26380  ofcfval4  26400  isrnmeas  26467  measdivcst  26492  sibfof  26573  sitgclg  26575  eulerpartlemsv2  26588  eulerpartlemsf  26589  eulerpartlemv  26594  eulerpartlemd  26596  eulerpartlemb  26598  eulerpartlemt  26601  eulerpartlemr  26604  eulerpartlemgvv  26606  eulerpartlemgu  26607  eulerpartlemgs2  26610  eulerpartlemn  26611  sseqfv2  26624  rrvdm  26676  cvmliftmolem1  27017  cvmliftlem3  27023  cvmliftlem10  27030  cvmliftlem13  27032  cvmlift2lem9  27047  cvmlift3lem6  27060  cvmlift3lem7  27061  ghomfo  27156  fprodss  27307  soseq  27561  nodmon  27637  heicant  28267  mbfresfi  28279  itg2addnclem  28284  itg2addnclem2  28285  cnicciblnc  28304  ftc1anclem1  28308  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem8  28315  ivthALT  28371  indexdom  28469  sdclem2  28479  cnres2  28503  sstotbnd2  28514  isbnd3  28524  ssbnd  28528  bnd2lem  28531  ismtyval  28540  exidreslem  28583  grpokerinj  28591  divrngcl  28604  isdrngo2  28605  keridl  28673  ismrcd1  28876  istopclsd  28878  mapfzcons2  28897  coeq0i  28933  pw2f1ocnv  29228  fnwe2lem2  29246  lmhmfgima  29279  fsuppeq  29292  pwfi2f1o  29293  cnioobibld  29431  itgpowd  29432  expgrowth  29451  cncmpmax  29596  stoweidlem29  29667  f0rn0  29984  wlkn0  30122  domnmsuppn0  30610  rmsuppss  30611  mndpsuppss  30612  scmsuppss  30613  bj-finsumval0  32156