Theorem fdm 5964

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5958	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 5904	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1475  dom cdm 5038   Fn wfn 5799  ⟶wf 5800

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 196  df-an 385  df-fn 5807  df-f 5808

This theorem is referenced by:  fdmi  5965  fssxp  5973  ffdm  5975  f00  6000  f0dom0  6002  f0rn0  6003  foima  6033  foco  6038  resdif  6070  fimacnv  6255  dff3  6280  ffvresb  6301  fmptco  6303  dmfex  7017  fornex  7028  frnsuppeq  7194  suppss  7212  onnseq  7328  issmo2  7333  smoiso  7346  mapprc  7748  elpm2r  7761  map0b  7782  mapsn  7785  brdomg  7851  pw2f1olem  7949  fopwdom  7953  fodomfib  8125  fisuppfi  8166  intrnfi  8205  ordtypelem5  8310  ordtypelem6  8311  ordtypelem7  8312  ordtypelem8  8313  wemapso2lem  8340  brwdomn0  8357  wdomtr  8363  cantnfcl  8447  cantnfle  8451  cantnflt  8452  cantnff  8454  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  cantnflem3  8471  cnfcomlem  8479  cnfcom  8480  cnfcom2lem  8481  cnfcom3lem  8483  cnfcom3  8484  iunmapdisj  8729  fseqenlem2  8731  fodomfi2  8766  infmap2  8923  coftr  8978  fin23lem30  9047  fin23lem40  9056  isf34lem5  9083  isf34lem7  9084  isf34lem6  9085  fin1a2lem7  9111  axdc3lem2  9156  axdc3lem4  9158  ttukeylem6  9219  fodomb  9229  pwxpndom2  9366  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  fseqsupcl  12638  fseqsupubi  12639  hashf1lem1  13096  wrddm  13167  swrdcl  13271  swrdnd2  13285  cats1un  13327  repswswrd  13382  limsupgle  14056  limsupgre  14060  rlim  14074  rlimi  14092  ello12  14095  lo1bdd  14099  elo12  14106  o1bdd  14110  lo1o1  14111  rlimclim  14125  rlimuni  14129  o1co  14165  rlimcn1  14167  isercolllem2  14244  isercolllem3  14245  fsumss  14303  fprodss  14517  ruclem11  14808  1arith  15469  vdwlem1  15523  vdwlem5  15527  vdwlem6  15528  vdwlem11  15533  ramval  15550  0ram  15562  0ram2  15563  0ramcl  15565  mrcuni  16104  homarcl2  16508  prfval  16662  intopsn  17076  gsumval  17094  gsumval2  17103  ghmrn  17496  ghmpreima  17505  cntzmhm2  17595  symgfixf1  17680  f1omvdconj  17689  pmtrfconj  17709  pmtrdifellem1  17719  pmtrdifellem2  17720  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumzmhm  18160  gsumzoppg  18167  gsum2d  18194  dmdprdd  18221  dprdres  18250  dprdss  18251  dprdf1  18255  dmdprdsplitlem  18259  dprd2da  18264  dmdprdsplit2lem  18267  dmdprdsplit2  18268  dmdprdsplit  18269  dprdsplit  18270  dpjidcl  18280  ablfac1eulem  18294  ablfac1eu  18295  ablfaclem2  18308  ablfaclem3  18309  ablfac2  18311  lmhmpreima  18869  lmhmlsp  18870  mplcoe1  19286  mplcoe5  19289  psr1baslem  19376  gsumfsum  19632  evpmss  19751  regsumsupp  19787  pjdm2  19874  frlmlbs  19955  islindf2  19972  f1lindf  19980  islindf4  19996  mattpostpos  20079  mdetdiaglem  20223  decpmatval  20389  pmatcollpw3lem  20407  iinopn  20532  iscnp3  20858  lmbrf  20874  cnpnei  20878  cnclima  20882  iscncl  20883  cnntri  20885  cnclsi  20886  cncls2  20887  cncls  20888  cnntr  20889  cncnp  20894  cndis  20905  paste  20908  lmcnp  20918  cnt0  20960  cnt1  20964  cnhaus  20968  cncmp  21005  imacmp  21010  hauscmplem  21019  cnconn  21035  conima  21038  1stcfb  21058  1stccnp  21075  1stckgenlem  21166  kgencn  21169  kgencn3  21171  txcnpi  21221  txcnp  21233  txcnmpt  21237  prdstps  21242  xkohaus  21266  xkopt  21268  xkoco2cn  21271  xkococnlem  21272  qtopval2  21309  qtopcn  21327  qtopeu  21329  hmeores  21384  fbasrn  21498  fmval  21557  fmf  21559  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  cnflf2  21617  lmflf  21619  txflf  21620  cnextfval  21676  cnextcn  21681  clssubg  21722  ghmcnp  21728  tgphaus  21730  qustgplem  21734  tsmsval  21744  tsmsgsum  21752  ucncn  21899  psmetdmdm  21920  xmetdmdm  21950  metn0  21975  xmetres  21979  metres  21980  xmeter  22048  tmsval  22096  metcnp  22156  metustss  22166  metustid  22169  metustsym  22170  metustexhalf  22171  metustfbas  22172  cfilucfil  22174  metuel2  22180  restmetu  22185  isngp2  22211  evth  22566  lmmbrf  22868  iscfil2  22872  caufval  22881  iscau2  22883  iscauf  22886  caucfil  22889  equivcau  22906  lmclimf  22910  rrxcph  22988  rrxsuppss  22994  ovollb2  23064  ovolunlem1a  23071  ovoliunlem1  23077  ovoliun2  23081  ioombl1lem4  23136  uniioombllem1  23155  uniioombllem2  23157  uniioombllem6  23162  mbfconstlem  23202  ismbf  23203  ismbfcn  23204  mbfimaicc  23206  mbfmulc2lem  23220  mbfmulc2re  23221  mbfimaopn2  23230  cncombf  23231  mbfaddlem  23233  mbflimsup  23239  i1f0rn  23255  itg1addlem5  23273  itg1climres  23287  mbfmullem2  23297  ibl0  23359  cniccibl  23413  limcfval  23442  limcdif  23446  ellimc2  23447  ellimc3  23449  limccnp  23461  dvfval  23467  cpnord  23504  cpnres  23506  dvcmul  23513  dvcmulf  23514  dvnfre  23521  dvexp  23522  c1liplem1  23563  c1lip2  23565  dvgt0lem1  23569  dvcnvrelem1  23584  dvcnvrelem2  23585  mdegfval  23626  mdegleb  23628  mdegldg  23630  deg1mul3le  23680  plyco0  23752  plyeq0lem  23770  plyeq0  23771  plyaddlem1  23773  plymullem1  23774  dgrcl  23793  dgrub  23794  dgrlb  23796  plycpn  23848  vieta1lem1  23869  vieta1lem2  23870  aalioulem3  23893  taylfvallem1  23915  tayl0  23920  taylply2  23926  taylply  23927  dvtaylp  23928  dvntaylp  23929  dvntaylp0  23930  taylthlem1  23931  taylthlem2  23932  ulm2  23943  ulmss  23955  ulmdvlem1  23958  ulmdvlem2  23959  ulmdvlem3  23960  itgulm  23966  xrlimcnp  24495  basellem5  24611  dchrelbas2  24762  dchrghm  24781  dchrptlem1  24789  dchrptlem2  24790  iscgrgd  25208  iscgrglt  25209  trgcgrg  25210  tgcgr4  25226  motcgrg  25239  eedimeq  25578  axcontlem10  25653  wrdupgr  25752  wrdumgr  25763  upgr1e  25779  uhgraun  25840  wrdumgra  25845  umgra1  25855  umgraun  25857  wlkn0  26055  eupares  26502  grporndm  26748  sspn  26975  dmadjrnb  28149  elnlfn  28171  xppreima  28829  fmptcof2  28839  curry2ima  28869  fpwrelmap  28896  smatrcl  29190  mdetpmtr1  29217  locfinreflem  29235  hauseqcn  29269  rge0scvg  29323  indpreima  29414  indf1ofs  29415  esumpcvgval  29467  ofcfval4  29494  isrnmeas  29590  measdivcst  29615  omsfval  29683  omscl  29684  omsf  29685  oms0  29686  omsmon  29687  omssubaddlem  29688  omssubadd  29689  carsgval  29692  carsggect  29707  omsmeas  29712  sibfof  29729  sitgclg  29731  eulerpartlemsv2  29747  eulerpartlemsf  29748  eulerpartlemv  29753  eulerpartlemd  29755  eulerpartlemb  29757  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemgvv  29765  eulerpartlemgu  29766  eulerpartlemgs2  29769  eulerpartlemn  29770  sseqfv2  29783  rrvdm  29835  cvmliftmolem1  30517  cvmliftlem3  30523  cvmliftlem10  30530  cvmliftlem13  30532  cvmlift2lem9  30547  cvmlift3lem6  30560  cvmlift3lem7  30561  mrsubfval  30659  mclsax  30720  mclsppslem  30734  mclspps  30735  soseq  30995  nodmon  31047  fwddifval  31439  fwddifnval  31440  ivthALT  31500  bj-finsumval0  32324  curf  32557  uncf  32558  curunc  32561  unccur  32562  matunitlindflem2  32576  ptrecube  32579  heicant  32614  mbfresfi  32626  itg2addnclem  32631  itg2addnclem2  32632  cnicciblnc  32651  ftc1anclem1  32655  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem8  32662  indexdom  32699  sdclem2  32708  cnres2  32732  sstotbnd2  32743  isbnd3  32753  ssbnd  32757  bnd2lem  32760  ismtyval  32769  ismgmOLD  32819  ismndo2  32843  exidreslem  32846  grpokerinj  32862  rngosn3  32893  rngodm1dm2  32901  divrngcl  32926  isdrngo2  32927  keridl  33001  ismrcd1  36279  istopclsd  36281  mapfzcons2  36300  coeq0i  36334  pw2f1ocnv  36622  fnwe2lem2  36639  lmhmfgima  36672  pwfi2f1o  36684  cnioobibld  36818  itgpowd  36819  wnefimgd  37480  funfvima2d  37491  binomcxplemnotnn0  37577  cncmpmax  38214  fresin2  38347  mapsnd  38383  fdmd  38415  evthiccabs  38565  mullimcf  38690  cncfuni  38772  cncficcgt0  38774  cncfioobd  38783  dvsinax  38801  dvsubcncf  38814  dvmulcncf  38815  dvdivcncf  38817  cnbdibl  38854  itgperiod  38873  fvvolioof  38882  fvvolicof  38884  stoweidlem29  38922  fourierdlem20  39020  fourierdlem48  39047  fourierdlem49  39048  fourierdlem53  39052  fourierdlem58  39057  fourierdlem59  39058  fourierdlem63  39062  fourierdlem68  39067  fourierdlem71  39070  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem80  39079  fourierdlem81  39080  fourierdlem82  39081  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem94  39093  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fouriercn  39125  sge0val  39259  fge0iccico  39263  sge0sn  39272  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0isum  39320  ismeannd  39360  isomennd  39421  hoicvr  39438  dmovn  39494  hspmbl  39519  ovolval4lem1  39539  ovnovollem1  39546  ovnovollem2  39547  fmtnoinf  39986  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  1wlkn0  40825  1wlkres  40879  1wlkp1lem1  40882  pthdivtx  40935  domnmsuppn0  41944  rmsuppss  41945  mndpsuppss  41946  scmsuppss  41947  fdivmpt  42132  fdivmptf  42133  refdivmptf  42134  fdivpm  42135  refdivpm  42136  elbigo2  42144  elbigolo1  42149