Theorem fdm 6714

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 29-May-2024.)

Assertion

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

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 6705	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6642	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5654  ⟶wf 6526

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 207  df-an 396  df-fn 6533  df-f 6534

This theorem is referenced by:  fdmd  6715  fdmi  6716  fimacnv  6727  fssxp  6732  ffdm  6734  f00  6759  f0dom0  6761  f0rn0  6762  fimadmfo  6798  fimadmfoALT  6800  focofo  6802  feldmfvelcdm  7075  dff3  7089  ffvresb  7114  dmfex  7899  fiun  7939  soseq  8156  fsuppeq  8172  fsuppeqg  8173  issmo2  8361  smoiso  8374  mapprc  8842  elpm2r  8857  map0b  8895  mapsnd  8898  brdomg  8969  brdomgOLD  8970  pw2f1olem  9088  iunmapdisj  10035  fodomfi2  10072  infmap2  10229  coftr  10285  fin23lem40  10363  isf34lem7  10391  axdc3lem2  10463  axdc3lem4  10465  rpnnen1lem4  12994  rpnnen1lem5  12995  fseqsupcl  13993  fseqsupubi  13994  ello12  15530  lo1bdd  15534  elo12  15541  o1bdd  15545  lo1o1  15546  rlimclim  15560  ramval  17026  0ram2  17039  0ramcl  17041  intopsn  18630  mndpsuppss  18741  symgfixf1  19416  f1omvdconj  19425  pmtrdifellem1  19455  pmtrdifellem2  19456  gsumval3  19886  dprdss  20010  dmdprdsplitlem  20018  ablfaclem3  20068  evpmss  21544  pjdm2  21669  islindf2  21772  islindf4  21796  decpmatval  22701  pmatcollpw3lem  22719  iscnp3  23180  cnpnei  23200  cncls2  23209  cncls  23210  cnntr  23211  cncnp  23216  cndis  23227  paste  23230  cncmp  23328  imacmp  23333  hauscmplem  23342  cnconn  23358  kgencn  23492  xkopt  23591  xkococnlem  23595  fbasrn  23820  fmval  23879  fmf  23881  rnelfmlem  23888  rnelfm  23889  cnflf2  23939  psmetdmdm  24242  xmetres  24301  metres  24302  metcnp  24478  metustsym  24492  cfilucfil  24496  metuel2  24502  iscauf  25230  equivcau  25250  lmclimf  25254  ismbf  25579  ismbfcn  25580  mbfimaicc  25582  mbfimaopn2  25608  ibl0  25738  cniccibl  25792  cnicciblnc  25794  dvnfre  25906  c1liplem1  25951  c1lip2  25953  dvcnvrelem2  25973  plyco0  26147  plyeq0  26166  vieta1lem2  26269  ulm2  26344  ulmss  26356  ulmdvlem2  26360  ulmdvlem3  26361  itgulm  26367  basellem5  27045  nodmon  27612  eedimeq  28823  axcontlem10  28898  wlkn0  29547  wlkres  29596  wlkp1lem1  29599  pthdivtx  29655  cyclnumvtx  29728  dmadjrnb  31833  elnlfn  31855  xppreima  32569  indpreima  32788  symgcom2  33041  tocyc01  33075  tocyccntz  33101  elrspunidl  33389  smatrcl  33773  mdetpmtr1  33800  locfinreflem  33817  hauseqcn  33875  rge0scvg  33926  isrnmeas  34177  omsfval  34272  omscl  34273  omsf  34274  eulerpartlemv  34342  eulerpartlemd  34344  eulerpartlemb  34346  eulerpartlemr  34352  eulerpartlemgvv  34354  eulerpartlemgs2  34358  eulerpartlemn  34359  rpsqrtcn  34571  cvmlift2lem9  35279  cvmlift3lem7  35293  mrsubfval  35476  ivthALT  36299  curf  37568  uncf  37569  unccur  37573  matunitlindflem2  37587  ptrecube  37590  heicant  37625  mbfresfi  37636  itg2addnclem  37641  itg2addnclem2  37642  ftc1anclem1  37663  indexdom  37704  sdclem2  37712  cnres2  37733  sstotbnd2  37744  bnd2lem  37761  ismgmOLD  37820  ismndo2  37844  exidreslem  37847  rngosn3  37894  rngodm1dm2  37902  rhmqusspan  42144  coeq0i  42723  pw2f1ocnv  43008  cnioobibld  43185  dfno2  43399  fresin2  45144  evthiccabs  45473  dvsubcncf  45901  dvmulcncf  45902  dvdivcncf  45904  cnbdibl  45939  fourierdlem48  46131  fourierdlem49  46132  fourierdlem58  46141  fourierdlem59  46142  fourierdlem71  46154  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem80  46163  fourierdlem81  46164  fourierdlem89  46172  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem94  46177  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fouriercn  46209  sge0val  46343  fge0iccico  46347  isomennd  46508  3f1oss1  47052  fafv2elrnb  47212  fmtnoinf  47498  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  upgrimwlklem2  47859  upgrimwlklem3  47860  upgrimtrlslem2  47866  cycl3grtri  47907  domnmsuppn0  48292  scmsuppss  48294  fdivmpt  48468  fdivmptf  48469  refdivmptf  48470  fdivpm  48471  refdivpm  48472  elbigo2  48480  elbigolo1  48485