Theorem fdm 6712

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5655  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6536  df-f 6537

This theorem is used by:  fdmd  6713  fdmi  6714  fimacnv  6725  fssxp  6730  ffdm  6732  f00  6757  f0dom0  6759  f0rn0  6760  fimadmfo  6798  fimadmfoALT  6800  focofo  6802  feldmfvelcdm  7079  dff3  7093  ffvresb  7119  dmfex  7902  fiun  7940  soseq  8157  fsuppeq  8173  fsuppeqg  8174  issmo2  8338  smoiso  8351  mapprc  8830  elpm2r  8844  curf  8869  uncf  8870  map0b  8890  mapsnd  8893  brdomg  8964  pw2f1olem  9079  iunmapdisj  10026  fodomfi2  10063  infmap2  10219  coftr  10275  fin23lem40  10353  isf34lem7  10381  axdc3lem2  10453  axdc3lem4  10455  rpnnen1lem4  13030  rpnnen1lem5  13031  fseqsupcl  14041  fseqsupubi  14042  ello12  15603  lo1bdd  15607  elo12  15614  o1bdd  15618  lo1o1  15619  rlimclim  15633  ramval  17100  0ram2  17113  0ramcl  17115  intopsn  18746  mndpsuppss  18872  symgfixf1  19564  f1omvdconj  19573  pmtrdifellem1  19603  pmtrdifellem2  19604  gsumval3  20034  dprdss  20158  dmdprdsplitlem  20166  ablfaclem3  20216  evpmss  21799  pjdm2  21924  islindf2  22027  islindf4  22051  matunitlindflem2  22902  decpmatval  22990  pmatcollpw3lem  23008  iscnp3  23469  cnpnei  23489  cncls2  23498  cncls  23499  cnntr  23500  cncnp  23505  cndis  23516  paste  23519  cncmp  23617  imacmp  23622  hauscmplem  23631  cnconn  23647  kgencn  23782  xkopt  23881  xkococnlem  23885  fbasrn  24110  fmval  24169  fmf  24171  rnelfmlem  24178  rnelfm  24179  cnflf2  24229  psmetdmdm  24531  xmetres  24590  metres  24591  metcnp  24767  metustsym  24781  cfilucfil  24785  metuel2  24791  iscauf  25508  equivcau  25528  lmclimf  25532  ismbf  25856  ismbfcn  25857  mbfimaicc  25859  mbfimaopn2  25885  ibl0  26014  cniccibl  26068  cnicciblnc  26070  dvnfre  26179  c1liplem1  26223  c1lip2  26225  dvcnvrelem2  26245  plyco0  26417  plyeq0  26437  vieta1lem2  26543  ulm2  26621  ulmss  26633  ulmdvlem2  26637  ulmdvlem3  26638  itgulm  26644  basellem5  27321  nodmon  27886  newbdayim  28168  eedimeq  29355  axcontlem10  29430  wlkn0  30080  wlkres  30128  wlkp1lem1  30131  pthdivtx  30191  cyclnumvtx  30267  dmadjrnb  32387  elnlfn  32409  xppreima  33118  indpreima  33311  symgcom2  33524  tocyc01  33558  tocyccntz  33584  elrspunidl  33856  smatrcl  34306  mdetpmtr1  34333  locfinreflem  34350  hauseqcn  34408  rge0scvg  34459  isrnmeas  34711  omsfval  34805  omscl  34806  omsf  34807  eulerpartlemv  34875  eulerpartlemd  34877  eulerpartlemb  34879  eulerpartlemr  34885  eulerpartlemgvv  34887  eulerpartlemgs2  34891  eulerpartlemn  34892  rpsqrtcn  35101  cvmlift2lem9  35890  cvmlift3lem7  35904  mrsubfval  36087  ivthALT  36954  unccur  38357  ptrecube  38369  heicant  38404  mbfresfi  38415  itg2addnclem  38420  itg2addnclem2  38421  ftc1anclem1  38442  indexdom  38484  sdclem2  38492  cnres2  38513  sstotbnd2  38524  bnd2lem  38541  ismgmOLD  38600  ismndo2  38624  exidreslem  38627  rngosn3  38674  rngodm1dm2  38682  rhmqusspan  43051  coeq0i  43598  pw2f1ocnv  43878  cnioobibld  44055  dfno2  44268  fresin2  46004  evthiccabs  46326  dvsubcncf  46752  dvmulcncf  46753  dvdivcncf  46755  cnbdibl  46790  fourierdlem48  46982  fourierdlem49  46983  fourierdlem58  46992  fourierdlem59  46993  fourierdlem71  47005  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem80  47014  fourierdlem81  47015  fourierdlem89  47023  fourierdlem91  47025  fourierdlem92  47026  fourierdlem93  47027  fourierdlem94  47028  fourierdlem111  47045  fourierdlem112  47046  fourierdlem113  47047  fouriercn  47060  sge0val  47194  fge0iccico  47198  isomennd  47359  tannpoly  47758  3f1oss1  47963  fafv2elrnb  48123  fmtnoinf  48439  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  upgrimwlklem2  48814  upgrimwlklem3  48815  upgrimtrlslem2  48821  cycl3grtri  48863  domnmsuppn0  49299  scmsuppss  49301  fdivmpt  49470  fdivmptf  49471  refdivmptf  49472  fdivpm  49473  refdivpm  49474  elbigo2  49482  elbigolo1  49487  xpco2  49785