Theorem fdm 5750

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

Syntax hints:   -> wi 4   = wceq 1437   dom cdm 4854   Fn wfn 5596   -->wf 5597

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 188  df-an 372  df-fn 5604  df-f 5605

This theorem is referenced by:  fdmi  5751  fssxp  5758  ffdm  5760  f00  5782  f0dom0  5784  f0rn0  5785  foima  5815  foco  5820  resdif  5851  fimacnv  6027  dff3  6050  ffvresb  6069  fmptco  6071  dmfex  6765  fornex  6776  frnsuppeq  6937  suppss  6956  onnseq  7071  issmo2  7076  smoiso  7089  mapprc  7484  elpm2r  7497  map0b  7518  mapsn  7521  brdomg  7587  pw2f1olem  7682  fopwdom  7686  fodomfib  7857  fisuppfi  7897  intrnfi  7936  ordtypelem5  8037  ordtypelem6  8038  ordtypelem7  8039  ordtypelem8  8040  wemapso2lem  8067  brwdomn0  8084  wdomtr  8090  cantnfcl  8171  cantnfle  8175  cantnflt  8176  cantnff  8178  cantnfp1lem3  8184  cantnflem1b  8190  cantnflem1d  8192  cantnflem1  8193  cantnflem3  8195  cnfcomlem  8203  cnfcom  8204  cnfcom2lem  8205  cnfcom3lem  8207  cnfcom3  8208  iunmapdisj  8452  fseqenlem2  8454  fodomfi2  8489  infmap2  8646  coftr  8701  fin23lem30  8770  fin23lem40  8779  isf34lem5  8806  isf34lem7  8807  isf34lem6  8808  fin1a2lem7  8834  axdc3lem2  8879  axdc3lem4  8881  ttukeylem6  8942  fodomb  8952  pwxpndom2  9089  rpnnen1lem4  11293  rpnnen1lem5  11294  fseqsupcl  12187  fseqsupubi  12188  hashimarn  12605  hashfzdm  12607  hashfirdm  12609  hashf1lem1  12613  wrddm  12665  swrdcl  12760  swrdnd2  12774  cats1un  12817  repswswrd  12872  limsupgle  13513  limsupgre  13520  limsupgreOLD  13521  rlim  13537  rlimi  13555  ello12  13558  lo1bdd  13562  elo12  13569  o1bdd  13573  lo1o1  13574  rlimclim  13588  rlimuni  13592  o1co  13628  rlimcn1  13630  isercolllem2  13707  isercolllem3  13708  fsumss  13769  fprodss  13980  ruclem11  14270  1arith  14825  vdwlem1  14885  vdwlem5  14889  vdwlem6  14890  vdwlem11  14895  ramval  14914  ramvalOLD  14915  0ram  14932  0ram2  14933  0ramcl  14935  mrcuni  15469  homarcl2  15872  prfval  16026  intopsn  16440  gsumval  16456  gsumval2  16465  ghmrn  16838  ghmpreima  16846  cntzmhm2  16935  symgfixf1  17020  f1omvdconj  17029  pmtrfconj  17049  pmtrdifellem1  17059  pmtrdifellem2  17060  gsumval3lem1  17465  gsumval3lem2  17466  gsumval3  17467  gsumzres  17469  gsumzcl2  17470  gsumzf1o  17472  gsumzaddlem  17480  gsumzmhm  17496  gsumzoppg  17503  gsum2d  17530  dmdprdd  17557  dprdres  17587  dprdss  17588  dprdf1  17592  dmdprdsplitlem  17596  dprd2da  17601  dmdprdsplit2lem  17604  dmdprdsplit2  17605  dmdprdsplit  17606  dprdsplit  17607  dpjidcl  17617  ablfac1eulem  17631  ablfac1eu  17632  ablfaclem2  17645  ablfaclem3  17646  ablfac2  17648  lmhmpreima  18197  lmhmlsp  18198  mplcoe1  18615  mplcoe5  18618  psr1baslem  18704  gsumfsum  18960  evpmss  19076  regsumsupp  19112  pjdm2  19196  frlmlbs  19277  islindf2  19294  f1lindf  19302  islindf4  19318  mattpostpos  19401  mdetdiaglem  19545  decpmatval  19711  pmatcollpw3lem  19729  iinopn  19854  iscnp3  20182  lmbrf  20198  cnpnei  20202  cnclima  20206  iscncl  20207  cnntri  20209  cnclsi  20210  cncls2  20211  cncls  20212  cnntr  20213  cncnp  20218  cndis  20229  paste  20232  lmcnp  20242  cnt0  20284  cnt1  20288  cnhaus  20292  cncmp  20329  imacmp  20334  hauscmplem  20343  cnconn  20359  conima  20362  1stcfb  20382  1stccnp  20399  1stckgenlem  20490  kgencn  20493  kgencn3  20495  txcnpi  20545  txcnp  20557  txcnmpt  20561  prdstps  20566  xkohaus  20590  xkopt  20592  xkoco2cn  20595  xkococnlem  20596  qtopval2  20633  qtopcn  20651  qtopeu  20653  hmeores  20708  fbasrn  20821  fmval  20880  fmf  20882  rnelfmlem  20889  rnelfm  20890  fmfnfmlem2  20892  fmfnfmlem4  20894  fmfnfm  20895  cnflf2  20940  lmflf  20942  txflf  20943  cnextfval  20999  cnextcn  21004  clssubg  21045  ghmcnp  21051  tgphaus  21053  qustgplem  21057  tsmsval  21067  tsmsgsum  21075  ucncn  21222  psmetdmdm  21243  xmetdmdm  21272  metn0  21297  xmetres  21301  metres  21302  xmeter  21370  tmsval  21418  metcnp  21478  metustss  21488  metustid  21491  metustsym  21492  metustexhalf  21493  metustfbas  21494  cfilucfil  21496  metuel2  21502  restmetu  21507  isngp2  21533  evth  21874  lmmbrf  22116  iscfil2  22120  caufval  22129  iscau2  22131  iscauf  22134  caucfil  22137  equivcau  22154  lmclimf  22157  rrxcph  22235  rrxsuppss  22241  ovollb2  22311  ovolunlem1a  22318  ovoliunlem1  22324  ovoliun2  22328  ioombl1lem4  22382  uniioombllem1  22406  uniioombllem2  22408  uniioombllem2OLD  22409  uniioombllem6  22414  mbfconstlem  22453  ismbf  22454  ismbfcn  22455  mbfimaicc  22457  mbfmulc2lem  22471  mbfmulc2re  22472  mbfimaopn2  22481  cncombf  22482  mbfaddlem  22484  mbflimsup  22491  mbflimsupOLD  22492  i1f0rn  22508  itg1addlem5  22526  itg1climres  22540  mbfmullem2  22550  ibl0  22612  cniccibl  22666  limcfval  22695  limcdif  22699  ellimc2  22700  ellimc3  22702  limccnp  22714  dvfval  22720  cpnord  22757  cpnres  22759  dvcmul  22766  dvcmulf  22767  dvnfre  22774  dvexp  22775  c1liplem1  22816  c1lip2  22818  dvgt0lem1  22822  dvcnvrelem1  22837  dvcnvrelem2  22838  mdegfval  22879  mdegleb  22881  mdegldg  22883  deg1mul3le  22933  plyco0  23005  plyeq0lem  23023  plyeq0  23024  plyaddlem1  23026  plymullem1  23027  dgrcl  23046  dgrub  23047  dgrlb  23049  plycpn  23101  vieta1lem1  23122  vieta1lem2  23123  aalioulem3  23146  taylfvallem1  23168  tayl0  23173  taylply2  23179  taylply  23180  dvtaylp  23181  dvntaylp  23182  dvntaylp0  23183  taylthlem1  23184  taylthlem2  23185  ulm2  23196  ulmss  23208  ulmdvlem1  23211  ulmdvlem2  23212  ulmdvlem3  23213  itgulm  23219  xrlimcnp  23750  basellem5  23865  dchrelbas2  24019  dchrghm  24038  dchrptlem1  24046  dchrptlem2  24047  iscgrgd  24412  trgcgrg  24413  motcgrg  24440  eedimeq  24765  axcontlem10  24840  uhgraun  24875  wrdumgra  24880  umgra1  24890  umgraun  24892  wlkn0  25091  eupares  25539  grporndm  25774  resgrprn  25844  isabloda  25863  subgores  25868  ismgmOLD  25884  ismndo2  25909  ghsubgolemOLD  25934  rngodm1dm2  25982  rngosn3  25990  vcoprne  26034  nvdm  26126  sspn  26211  dmadjrnb  27385  elnlfn  27407  xppreima  28079  fmptcof2  28090  curry2ima  28120  fpwrelmap  28152  smatrcl  28452  mdetpmtr1  28479  locfinreflem  28497  hauseqcn  28531  rge0scvg  28585  indpreima  28676  indf1ofs  28677  esumpcvgval  28729  ofcfval4  28756  isrnmeas  28852  measdivcst  28877  omsfval  28946  omscl  28947  omsf  28948  oms0  28949  omsmon  28950  omssubaddlem  28951  omssubadd  28952  carsgval  28955  carsggect  28970  omsmeas  28975  sibfof  28992  sitgclg  28994  eulerpartlemsv2  29008  eulerpartlemsf  29009  eulerpartlemv  29014  eulerpartlemd  29016  eulerpartlemb  29018  eulerpartlemt  29021  eulerpartlemr  29024  eulerpartlemgvv  29026  eulerpartlemgu  29027  eulerpartlemgs2  29030  eulerpartlemn  29031  sseqfv2  29044  rrvdm  29096  cvmliftmolem1  29783  cvmliftlem3  29789  cvmliftlem10  29796  cvmliftlem13  29798  cvmlift2lem9  29813  cvmlift3lem6  29826  cvmlift3lem7  29827  mrsubfval  29925  mclsax  29986  mclsppslem  30000  mclspps  30001  ghomfo  30088  soseq  30270  nodmon  30315  fwddifval  30705  fwddifnval  30706  ivthALT  30767  bj-finsumval0  31438  ptrecube  31634  heicant  31669  mbfresfi  31681  itg2addnclem  31687  itg2addnclem2  31688  cnicciblnc  31707  ftc1anclem1  31711  ftc1anclem5  31715  ftc1anclem6  31716  ftc1anclem8  31718  indexdom  31755  sdclem2  31765  cnres2  31789  sstotbnd2  31800  isbnd3  31810  ssbnd  31814  bnd2lem  31817  ismtyval  31826  exidreslem  31869  grpokerinj  31877  divrngcl  31890  isdrngo2  31891  keridl  31959  ismrcd1  35239  istopclsd  35241  mapfzcons2  35260  coeq0i  35294  pw2f1ocnv  35588  fnwe2lem2  35605  lmhmfgima  35638  pwfi2f1o  35650  cnioobibld  35787  itgpowd  35788  wnefimgd  36227  funfvima2d  36239  binomcxplemnotnn0  36332  cncmpmax  36983  fresin2  37048  evthiccabs  37168  mullimcf  37265  cncfuni  37326  cncficcgt0  37328  cncfioobd  37337  dvsinax  37345  dvsubcncf  37358  dvmulcncf  37359  dvdivcncf  37361  cnbdibl  37398  itgperiod  37417  stoweidlem29  37448  stoweidlem29OLD  37449  fourierdlem20  37548  fourierdlem48  37576  fourierdlem49  37577  fourierdlem53  37581  fourierdlem58  37586  fourierdlem59  37587  fourierdlem63  37591  fourierdlem68  37596  fourierdlem71  37599  fourierdlem73  37601  fourierdlem74  37602  fourierdlem75  37603  fourierdlem76  37604  fourierdlem80  37608  fourierdlem81  37609  fourierdlem82  37610  fourierdlem89  37617  fourierdlem91  37619  fourierdlem92  37620  fourierdlem93  37621  fourierdlem94  37622  fourierdlem111  37639  fourierdlem112  37640  fourierdlem113  37641  fouriercn  37654  sge0val  37732  fge0iccico  37736  sge0sn  37745  sge0tsms  37746  sge0cl  37747  sge0f1o  37748  ismeannd  37804  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  uhgun  38440  domnmsuppn0  38904  rmsuppss  38905  mndpsuppss  38906  scmsuppss  38907  fdivmpt  39102  fdivmptf  39103  refdivmptf  39104  fdivpm  39105  refdivpm  39106  elbigo2  39114  elbigolo1  39119