Theorem fdm 6716

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 6706	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6641	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1567  dom cdm 5662  ⟶wf 6533

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 210  df-an 401  df-fn 6540  df-f 6541

This theorem is referenced by:  fdmd  6717  fdmi  6718  fimacnv  6729  fssxp  6734  ffdm  6736  f00  6761  f0dom0  6763  f0rn0  6764  fimadmfo  6802  fimadmfoALT  6804  focofo  6806  feldmfvelcdm  7082  dff3  7096  ffvresb  7122  dmfex  7901  fiun  7939  soseq  8154  fsuppeq  8170  fsuppeqg  8171  issmo2  8335  smoiso  8348  mapprc  8827  elpm2r  8841  map0b  8880  mapsnd  8883  brdomg  8954  pw2f1olem  9068  iunmapdisj  10006  fodomfi2  10043  infmap2  10199  coftr  10256  fin23lem40  10334  isf34lem7  10362  axdc3lem2  10434  axdc3lem4  10436  rpnnen1lem4  13003  rpnnen1lem5  13004  fseqsupcl  14012  fseqsupubi  14013  ello12  15566  lo1bdd  15570  elo12  15577  o1bdd  15581  lo1o1  15582  rlimclim  15596  ramval  17067  0ram2  17080  0ramcl  17082  intopsn  18711  mndpsuppss  18822  symgfixf1  19506  f1omvdconj  19515  pmtrdifellem1  19545  pmtrdifellem2  19546  gsumval3  19976  dprdss  20100  dmdprdsplitlem  20108  ablfaclem3  20158  evpmss  21704  pjdm2  21829  islindf2  21932  islindf4  21956  decpmatval  22890  pmatcollpw3lem  22908  iscnp3  23369  cnpnei  23389  cncls2  23398  cncls  23399  cnntr  23400  cncnp  23405  cndis  23416  paste  23419  cncmp  23517  imacmp  23522  hauscmplem  23531  cnconn  23547  kgencn  23681  xkopt  23780  xkococnlem  23784  fbasrn  24009  fmval  24068  fmf  24070  rnelfmlem  24077  rnelfm  24078  cnflf2  24128  psmetdmdm  24430  xmetres  24489  metres  24490  metcnp  24666  metustsym  24680  cfilucfil  24684  metuel2  24690  iscauf  25407  equivcau  25427  lmclimf  25431  ismbf  25755  ismbfcn  25756  mbfimaicc  25758  mbfimaopn2  25784  ibl0  25914  cniccibl  25968  cnicciblnc  25970  dvnfre  26079  c1liplem1  26123  c1lip2  26125  dvcnvrelem2  26145  plyco0  26317  plyeq0  26336  vieta1lem2  26440  ulm2  26513  ulmss  26525  ulmdvlem2  26529  ulmdvlem3  26530  itgulm  26536  basellem5  27214  nodmon  27779  newbdayim  28061  eedimeq  29188  axcontlem10  29263  wlkn0  29910  wlkres  29958  wlkp1lem1  29961  pthdivtx  30016  cyclnumvtx  30089  dmadjrnb  32198  elnlfn  32220  xppreima  32930  indpreima  33125  symgcom2  33344  tocyc01  33378  tocyccntz  33404  elrspunidl  33679  smatrcl  34130  mdetpmtr1  34157  locfinreflem  34174  hauseqcn  34232  rge0scvg  34283  isrnmeas  34534  omsfval  34628  omscl  34629  omsf  34630  eulerpartlemv  34698  eulerpartlemd  34700  eulerpartlemb  34702  eulerpartlemr  34708  eulerpartlemgvv  34710  eulerpartlemgs2  34714  eulerpartlemn  34715  rpsqrtcn  34924  cvmlift2lem9  35701  cvmlift3lem7  35715  mrsubfval  35898  ivthALT  36734  curf  38136  uncf  38137  unccur  38141  matunitlindflem2  38155  ptrecube  38158  heicant  38193  mbfresfi  38204  itg2addnclem  38209  itg2addnclem2  38210  ftc1anclem1  38231  indexdom  38272  sdclem2  38280  cnres2  38301  sstotbnd2  38312  bnd2lem  38329  ismgmOLD  38388  ismndo2  38412  exidreslem  38415  rngosn3  38462  rngodm1dm2  38470  rhmqusspan  42841  coeq0i  43375  pw2f1ocnv  43655  cnioobibld  43832  dfno2  44045  fresin2  45781  evthiccabs  46103  dvsubcncf  46529  dvmulcncf  46530  dvdivcncf  46532  cnbdibl  46567  fourierdlem48  46759  fourierdlem49  46760  fourierdlem58  46769  fourierdlem59  46770  fourierdlem71  46782  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem80  46791  fourierdlem81  46792  fourierdlem89  46800  fourierdlem91  46802  fourierdlem92  46803  fourierdlem93  46804  fourierdlem94  46805  fourierdlem111  46822  fourierdlem112  46823  fourierdlem113  46824  fouriercn  46837  sge0val  46971  fge0iccico  46975  isomennd  47136  tannpoly  47515  3f1oss1  47700  fafv2elrnb  47860  fmtnoinf  48176  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  upgrimwlklem2  48551  upgrimwlklem3  48552  upgrimtrlslem2  48558  cycl3grtri  48600  domnmsuppn0  49033  scmsuppss  49035  fdivmpt  49204  fdivmptf  49205  refdivmptf  49206  fdivpm  49207  refdivpm  49208  elbigo2  49216  elbigolo1  49221  xpco2  49519