Theorem fdm 6051

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

Syntax hints:   -> wi 4   = wceq 1483   dom cdm 5114   Fn wfn 5883   -->wf 5884

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 197  df-an 386  df-fn 5891  df-f 5892

This theorem is referenced by:  fdmi  6052  fssxp  6060  ffdm  6062  f00  6087  f0dom0  6089  f0rn0  6090  foima  6120  foco  6125  resdif  6157  fimacnv  6347  dff3  6372  ffvresb  6394  fmptco  6396  dmfex  7124  fornex  7135  frnsuppeq  7307  suppss  7325  onnseq  7441  issmo2  7446  smoiso  7459  mapprc  7861  elpm2r  7875  map0b  7896  mapsn  7899  brdomg  7965  pw2f1olem  8064  fopwdom  8068  fodomfib  8240  fisuppfi  8283  intrnfi  8322  ordtypelem5  8427  ordtypelem6  8428  ordtypelem7  8429  ordtypelem8  8430  wemapso2lem  8457  brwdomn0  8474  wdomtr  8480  cantnfcl  8564  cantnfle  8568  cantnflt  8569  cantnff  8571  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1d  8585  cantnflem1  8586  cantnflem3  8588  cnfcomlem  8596  cnfcom  8597  cnfcom2lem  8598  cnfcom3lem  8600  cnfcom3  8601  iunmapdisj  8846  fseqenlem2  8848  fodomfi2  8883  infmap2  9040  coftr  9095  fin23lem30  9164  fin23lem40  9173  isf34lem5  9200  isf34lem7  9201  isf34lem6  9202  fin1a2lem7  9228  axdc3lem2  9273  axdc3lem4  9275  ttukeylem6  9336  fodomb  9348  pwxpndom2  9487  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  fseqsupcl  12776  fseqsupubi  12777  hashf1lem1  13239  wrddm  13312  swrdcl  13419  swrdnd2  13433  cats1un  13475  repswswrd  13531  limsupgle  14208  limsupgre  14212  rlim  14226  rlimi  14244  ello12  14247  lo1bdd  14251  elo12  14258  o1bdd  14262  lo1o1  14263  rlimclim  14277  rlimuni  14281  o1co  14317  rlimcn1  14319  isercolllem2  14396  isercolllem3  14397  fsumss  14456  fprodss  14678  ruclem11  14969  1arith  15631  vdwlem1  15685  vdwlem5  15689  vdwlem6  15690  vdwlem11  15695  ramval  15712  0ram  15724  0ram2  15725  0ramcl  15727  mrcuni  16281  homarcl2  16685  prfval  16839  intopsn  17253  gsumval  17271  gsumval2  17280  ghmrn  17673  ghmpreima  17682  cntzmhm2  17772  symgfixf1  17857  f1omvdconj  17866  pmtrfconj  17886  pmtrdifellem1  17896  pmtrdifellem2  17897  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumzmhm  18337  gsumzoppg  18344  gsum2d  18371  dmdprdd  18398  dprdres  18427  dprdss  18428  dprdf1  18432  dmdprdsplitlem  18436  dprd2da  18441  dmdprdsplit2lem  18444  dmdprdsplit2  18445  dmdprdsplit  18446  dprdsplit  18447  dpjidcl  18457  ablfac1eulem  18471  ablfac1eu  18472  ablfaclem2  18485  ablfaclem3  18486  ablfac2  18488  lmhmpreima  19048  lmhmlsp  19049  mplcoe1  19465  mplcoe5  19468  psr1baslem  19555  gsumfsum  19813  evpmss  19932  regsumsupp  19968  pjdm2  20055  frlmlbs  20136  islindf2  20153  f1lindf  20161  islindf4  20177  mattpostpos  20260  mdetdiaglem  20404  decpmatval  20570  pmatcollpw3lem  20588  iinopn  20707  iscnp3  21048  lmbrf  21064  cnpnei  21068  cnclima  21072  iscncl  21073  cnntri  21075  cnclsi  21076  cncls2  21077  cncls  21078  cnntr  21079  cncnp  21084  cndis  21095  paste  21098  lmcnp  21108  cnt0  21150  cnt1  21154  cnhaus  21158  cncmp  21195  imacmp  21200  hauscmplem  21209  cnconn  21225  connima  21228  1stcfb  21248  1stccnp  21265  1stckgenlem  21356  kgencn  21359  kgencn3  21361  txcnpi  21411  txcnp  21423  txcnmpt  21427  prdstps  21432  xkohaus  21456  xkopt  21458  xkoco2cn  21461  xkococnlem  21462  qtopval2  21499  qtopcn  21517  qtopeu  21519  hmeores  21574  fbasrn  21688  fmval  21747  fmf  21749  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  cnflf2  21807  lmflf  21809  txflf  21810  cnextfval  21866  cnextcn  21871  clssubg  21912  ghmcnp  21918  tgphaus  21920  qustgplem  21924  tsmsval  21934  tsmsgsum  21942  ucncn  22089  psmetdmdm  22110  xmetdmdm  22140  metn0  22165  xmetres  22169  metres  22170  xmeter  22238  tmsval  22286  metcnp  22346  metustss  22356  metustid  22359  metustsym  22360  metustexhalf  22361  metustfbas  22362  cfilucfil  22364  metuel2  22370  restmetu  22375  isngp2  22401  evth  22758  lmmbrf  23060  iscfil2  23064  caufval  23073  iscau2  23075  iscauf  23078  caucfil  23081  equivcau  23098  lmclimf  23102  rrxcph  23180  rrxsuppss  23186  ovollb2  23257  ovolunlem1a  23264  ovoliunlem1  23270  ovoliun2  23274  ioombl1lem4  23329  uniioombllem1  23349  uniioombllem2  23351  uniioombllem6  23356  mbfconstlem  23396  ismbf  23397  ismbfcn  23398  mbfimaicc  23400  mbfmulc2lem  23414  mbfmulc2re  23415  mbfimaopn2  23424  cncombf  23425  mbfaddlem  23427  mbflimsup  23433  i1f0rn  23449  itg1addlem5  23467  itg1climres  23481  mbfmullem2  23491  ibl0  23553  cniccibl  23607  limcfval  23636  limcdif  23640  ellimc2  23641  ellimc3  23643  limccnp  23655  dvfval  23661  cpnord  23698  cpnres  23700  dvcmul  23707  dvcmulf  23708  dvnfre  23715  dvexp  23716  c1liplem1  23759  c1lip2  23761  dvgt0lem1  23765  dvcnvrelem1  23780  dvcnvrelem2  23781  mdegfval  23822  mdegleb  23824  mdegldg  23826  deg1mul3le  23876  plyco0  23948  plyeq0lem  23966  plyeq0  23967  plyaddlem1  23969  plymullem1  23970  dgrcl  23989  dgrub  23990  dgrlb  23992  plycpn  24044  vieta1lem1  24065  vieta1lem2  24066  aalioulem3  24089  taylfvallem1  24111  tayl0  24116  taylply2  24122  taylply  24123  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  taylthlem1  24127  taylthlem2  24128  ulm2  24139  ulmss  24151  ulmdvlem1  24154  ulmdvlem2  24155  ulmdvlem3  24156  itgulm  24162  xrlimcnp  24695  basellem5  24811  dchrelbas2  24962  dchrghm  24981  dchrptlem1  24989  dchrptlem2  24990  iscgrgd  25408  iscgrglt  25409  trgcgrg  25410  tgcgr4  25426  motcgrg  25439  eedimeq  25778  axcontlem10  25853  wrdupgr  25980  wrdumgr  25992  upgr1e  26008  wlkn0  26516  wlkres  26567  wlkp1lem1  26570  pthdivtx  26625  grporndm  27364  sspn  27591  dmadjrnb  28765  elnlfn  28787  xppreima  29449  fmptcof2  29457  curry2ima  29486  fpwrelmap  29508  smatrcl  29862  mdetpmtr1  29889  locfinreflem  29907  hauseqcn  29941  rge0scvg  29995  indpreima  30087  indf1ofs  30088  esumpcvgval  30140  ofcfval4  30167  isrnmeas  30263  measdivcst  30288  omsfval  30356  omscl  30357  omsf  30358  oms0  30359  omsmon  30360  omssubaddlem  30361  omssubadd  30362  carsgval  30365  carsggect  30380  omsmeas  30385  sibfof  30402  sitgclg  30404  eulerpartlemsv2  30420  eulerpartlemsf  30421  eulerpartlemv  30426  eulerpartlemd  30428  eulerpartlemb  30430  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemgvv  30438  eulerpartlemgu  30439  eulerpartlemgs2  30442  eulerpartlemn  30443  sseqfv2  30456  rrvdm  30508  rpsqrtcn  30671  ftc2re  30676  cvmliftmolem1  31263  cvmliftlem3  31269  cvmliftlem10  31276  cvmliftlem13  31278  cvmlift2lem9  31293  cvmlift3lem6  31306  cvmlift3lem7  31307  mrsubfval  31405  mclsax  31466  mclsppslem  31480  mclspps  31481  soseq  31751  nodmon  31803  fwddifval  32269  fwddifnval  32270  ivthALT  32330  bj-finsumval0  33147  curf  33387  uncf  33388  curunc  33391  unccur  33392  matunitlindflem2  33406  ptrecube  33409  heicant  33444  mbfresfi  33456  itg2addnclem  33461  itg2addnclem2  33462  cnicciblnc  33481  ftc1anclem1  33485  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem8  33492  indexdom  33529  sdclem2  33538  cnres2  33562  sstotbnd2  33573  isbnd3  33583  ssbnd  33587  bnd2lem  33590  ismtyval  33599  ismgmOLD  33649  ismndo2  33673  exidreslem  33676  grpokerinj  33692  rngosn3  33723  rngodm1dm2  33731  divrngcl  33756  isdrngo2  33757  keridl  33831  ismrcd1  37261  istopclsd  37263  mapfzcons2  37282  coeq0i  37316  pw2f1ocnv  37604  fnwe2lem2  37621  lmhmfgima  37654  pwfi2f1o  37666  cnioobibld  37799  itgpowd  37800  wnefimgd  38460  funfvima2d  38469  binomcxplemnotnn0  38555  cncmpmax  39191  fresin2  39352  mapsnd  39388  fdmd  39420  evthiccabs  39718  mullimcf  39855  cncfuni  40099  cncficcgt0  40101  cncfioobd  40110  dvsinax  40127  dvsubcncf  40139  dvmulcncf  40140  dvdivcncf  40142  cnbdibl  40178  itgperiod  40197  fvvolioof  40206  fvvolicof  40208  stoweidlem29  40246  fourierdlem20  40344  fourierdlem48  40371  fourierdlem49  40372  fourierdlem53  40376  fourierdlem58  40381  fourierdlem59  40382  fourierdlem63  40386  fourierdlem68  40391  fourierdlem71  40394  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem80  40403  fourierdlem81  40404  fourierdlem82  40405  fourierdlem89  40412  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem94  40417  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fouriercn  40449  sge0val  40583  fge0iccico  40587  sge0sn  40596  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0isum  40644  ismeannd  40684  isomennd  40745  hoicvr  40762  dmovn  40818  hspmbl  40843  ovolval4lem1  40863  ovnovollem1  40870  ovnovollem2  40871  fmtnoinf  41448  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  domnmsuppn0  42150  rmsuppss  42151  mndpsuppss  42152  scmsuppss  42153  fdivmpt  42334  fdivmptf  42335  refdivmptf  42336  fdivpm  42337  refdivpm  42338  elbigo2  42346  elbigolo1  42351