Theorem fdm 5554

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

Syntax hints:   -> wi 4   = wceq 1649   dom cdm 4837   Fn wfn 5408   -->wf 5409

This theorem is referenced by:  fdmi  5555  fssxp  5561  ffdm  5564  dmfex  5585  f00  5587  foima  5617  foco  5622  resdif  5655  fimacnv  5821  dff3  5841  ffvresb  5859  fmptco  5860  fornex  5929  onnseq  6565  issmo2  6570  smoiso  6583  mapprc  6981  elpm2r  6993  map0b  7011  mapsn  7014  brdomg  7077  pw2f1olem  7171  fopwdom  7175  fodomfib  7345  intrnfi  7379  ordtypelem5  7447  ordtypelem6  7448  ordtypelem7  7449  ordtypelem8  7450  wemapso2  7477  brwdomn0  7493  wdomtr  7499  cantnfcl  7578  cantnfle  7582  cantnflt  7583  cantnff  7585  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  cantnflem3  7603  cnfcomlem  7612  cnfcom  7613  cnfcom2lem  7614  cnfcom3lem  7616  cnfcom3  7617  iunmapdisj  7860  fseqenlem2  7862  fodomfi2  7897  infmap2  8054  coftr  8109  fin23lem30  8178  fin23lem40  8187  isf34lem5  8214  isf34lem7  8215  isf34lem6  8216  fin1a2lem7  8242  axdc3lem2  8287  axdc3lem4  8289  ttukeylem6  8350  fodomb  8360  pwxpndom2  8496  nn0supp  10229  rpnnen1lem4  10559  rpnnen1lem5  10560  fseqsupcl  11271  fseqsupubi  11272  hashf1lem1  11659  swrdcl  11721  swrdval2  11722  cats1un  11745  limsupgle  12226  limsupgre  12230  rlim  12244  rlimi  12262  ello12  12265  lo1bdd  12269  elo12  12276  o1bdd  12280  lo1o1  12281  rlimclim  12295  rlimuni  12299  lo1eq  12317  rlimeq  12318  rlimcld2  12327  o1co  12335  rlimcn1  12337  rlimcn2  12339  rlimsqzlem  12397  isercolllem2  12414  isercolllem3  12415  fsumss  12474  ruclem11  12794  1arith  13250  vdwlem1  13304  vdwlem5  13308  vdwlem6  13309  vdwlem11  13314  ramval  13331  0ram  13343  0ram2  13344  0ramcl  13346  mrcuni  13801  homarcl2  14145  prfval  14251  fisuppfi  14728  gsumval  14730  gsumval2  14738  ghmrn  14974  ghmpreima  14982  cntzmhm2  15093  gsumval3  15469  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumzmhm  15488  gsumzoppg  15494  gsum2d  15501  dmdprdd  15515  dprdres  15541  dprdss  15542  dprdz  15543  dprdf1  15546  dmdprdsplitlem  15550  dprd2da  15555  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dmdprdsplit  15560  dprdsplit  15561  dpjidcl  15571  ablfac1eulem  15585  ablfac1eu  15586  ablfaclem2  15599  ablfaclem3  15600  ablfac2  15602  lmhmpreima  16079  lmhmlsp  16080  mplcoe1  16483  mplcoe2  16485  psr1baslem  16538  gsumfsum  16721  pjdm2  16893  iinopn  16930  iscnp3  17262  lmbrf  17278  cnpnei  17282  cnclima  17286  iscncl  17287  cnntri  17289  cnclsi  17290  cncls2  17291  cncls  17292  cnntr  17293  cncnp  17298  cnrest  17303  cndis  17309  paste  17312  lmcnp  17322  cnt0  17364  cnt1  17368  cnhaus  17372  cncmp  17409  imacmp  17414  hauscmplem  17423  cnconn  17438  conima  17441  1stcfb  17461  1stccnp  17478  1stckgenlem  17538  kgencn  17541  kgencn3  17543  txcnpi  17593  txcnp  17605  txcnmpt  17609  prdstps  17614  xkohaus  17638  xkopt  17640  xkoco2cn  17643  xkococnlem  17644  qtopval2  17681  qtopcn  17699  qtopeu  17701  hmeores  17756  fbasrn  17869  fmval  17928  fmf  17930  rnelfmlem  17937  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  cnflf2  17988  lmflf  17990  txflf  17991  alexsublem  18028  cnextfval  18046  cnextcn  18051  clssubg  18091  ghmcnp  18097  tgphaus  18099  divstgplem  18103  tsmsval  18113  tsmsgsum  18121  ucncn  18268  psmetdmdm  18289  xmetdmdm  18318  metn0  18343  xmetres  18347  metres  18348  xmeter  18416  tmsval  18464  metcnp  18524  metustssOLD  18536  metustss  18537  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustsym  18545  metustexhalfOLD  18546  metustexhalf  18547  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  metuel2  18562  restmetu  18570  isngp2  18597  evth  18937  lmmbrf  19168  iscfil2  19172  caufval  19181  iscau2  19183  iscauf  19186  caucfil  19189  cmetcaulem  19194  equivcau  19206  lmclimf  19209  minveclem3b  19282  ovollb2  19338  ovolunlem1a  19345  ovoliunlem1  19351  ovoliun2  19355  ioombl1lem4  19408  uniioombllem1  19426  uniioombllem2  19428  uniioombllem6  19433  mbfconstlem  19474  ismbf  19475  ismbfcn  19476  mbfimaicc  19478  mbfmulc2lem  19492  mbfmulc2re  19493  mbfneg  19495  mbfimaopn2  19502  cncombf  19503  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  mbflimsup  19511  i1f0rn  19527  itg1addlem5  19545  itg1climres  19559  mbfmullem2  19569  itg2monolem1  19595  itg2mono  19598  itg2i1fseq2  19601  itg2cnlem1  19606  isibl2  19611  ibl0  19631  cniccibl  19685  limcfval  19712  limcdif  19716  ellimc2  19717  ellimc3  19719  limccnp  19731  limccnp2  19732  limcco  19733  dvfval  19737  cpnord  19774  cpnres  19776  dvcmul  19783  dvcmulf  19784  dvnfre  19791  dvexp  19792  c1liplem1  19833  c1lip2  19835  dvgt0lem1  19839  dvcnvrelem1  19854  dvcnvrelem2  19855  itgsubstlem  19885  mdegfval  19938  mdegleb  19940  mdegldg  19942  deg1mul3le  19992  plyco0  20064  plyeq0lem  20082  plyeq0  20083  plyaddlem1  20085  plymullem1  20086  dgrcl  20105  dgrub  20106  dgrlb  20108  plycpn  20159  vieta1lem1  20180  vieta1lem2  20181  aalioulem3  20204  taylfvallem1  20226  tayl0  20231  taylply2  20237  taylply  20238  dvtaylp  20239  dvntaylp  20240  dvntaylp0  20241  taylthlem1  20242  taylthlem2  20243  ulm2  20254  ulmss  20266  ulmdvlem1  20269  ulmdvlem2  20270  ulmdvlem3  20271  iblulm  20276  itgulm  20277  rlimcnp2  20758  xrlimcnp  20760  basellem5  20820  dchrelbas2  20974  dchrghm  20993  dchrptlem1  21001  dchrptlem2  21002  dchrisumlema  21135  uhgraun  21299  wrdumgra  21304  umgra1  21314  umgraun  21316  eupares  21650  grporndm  21751  resgrprn  21821  isabloda  21840  subgores  21845  ismgm  21861  ismndo2  21886  ghsubgolem  21911  rngodm1dm2  21959  rngosn3  21967  vcoprne  22011  nvdm  22103  sspn  22188  htthlem  22373  dmadjrnb  23362  elnlfn  23384  xppreima  24012  fmptcof2  24029  curry2ima  24050  hauseqcn  24246  rge0scvg  24288  indpreima  24375  indf1ofs  24376  esumpcvgval  24421  ofcfval4  24441  isrnmeas  24507  measdivcst  24532  sibfof  24607  sitgclg  24609  rrvdm  24657  cvmliftmolem1  24921  cvmliftlem3  24927  cvmliftlem10  24934  cvmliftlem13  24936  cvmlift2lem9  24951  cvmlift3lem6  24964  cvmlift3lem7  24965  ghomfo  25055  fprodss  25227  soseq  25468  nodmon  25518  eedimeq  25741  axcontlem10  25816  mbfresfi  26152  itg2addnclem  26155  itg2addnclem2  26156  cnicciblnc  26175  ivthALT  26228  indexdom  26326  sdclem2  26336  cnres2  26362  sstotbnd2  26373  isbnd3  26383  ssbnd  26387  bnd2lem  26390  ismtyval  26399  exidreslem  26442  grpokerinj  26450  divrngcl  26463  isdrngo2  26464  keridl  26532  ismrcd1  26642  istopclsd  26644  mapfzcons2  26665  coeq0i  26701  pw2f1ocnv  26998  fnwe2lem2  27016  lmhmfgima  27050  fsuppeq  27127  pwfi2f1o  27128  islindf2  27152  f1lindf  27160  f1omvdconj  27257  pmtrfconj  27275  expgrowth  27420  cncmpmax  27570  stoweidlem29  27645  hashimarn  27994  hashfirdm  27996  hashfzdm  27997  swrdnd  28001

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-fn 5416  df-f 5417