Theorem fndmi 6602

Description: The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)

Hypothesis

Ref	Expression
fndmi.1	⊢ 𝐹 Fn 𝐴

Assertion

Ref	Expression
fndmi	⊢ dom 𝐹 = 𝐴

Proof of Theorem fndmi

Step	Hyp	Ref	Expression
1		fndmi.1	. 2 ⊢ 𝐹 Fn 𝐴
2		fndm 6601	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1542  dom cdm 5631   Fn wfn 6493

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 6501

This theorem is referenced by:  dmmpti  6642  dmmpo  8024  tfr2  8337  tz7.44-2  8346  rdgsuc  8363  tz7.48-2  8381  tz7.48-1  8382  tz7.48-3  8383  tz7.49  8384  brwitnlem  8442  om0x  8454  naddcllem  8612  naddov2  8615  naddasslem1  8630  naddasslem2  8631  elpmi  8793  elmapex  8795  pmresg  8818  pmsspw  8825  r1suc  9694  r1ord  9704  r1ord3  9706  onwf  9754  r1val3  9762  r1pw  9769  rankr1b  9788  alephcard  9992  alephnbtwn  9993  alephgeom  10004  dfac12lem2  10067  alephsing  10198  hsmexlem6  10353  zorn2lem4  10421  alephadd  10500  alephreg  10505  pwcfsdom  10506  r1limwun  10659  r1wunlim  10660  rankcf  10700  inatsk  10701  r1tskina  10705  dmaddpi  10813  dmmulpi  10814  seqexw  13979  hashkf  14294  bpolylem  16013  0rest  17392  firest  17395  homfeqbas  17662  cidpropd  17676  2oppchomf  17690  fucbas  17930  fuchom  17931  xpccofval  18148  oppchofcl  18226  oyoncl  18236  ex-chn2  18604  mulgfval  19045  gicer  19252  psgneldm  19478  psgneldm2  19479  psgnval  19482  psgnghm  21560  psgnghm2  21561  cldrcl  22991  iscldtop  23060  restrcl  23122  ssrest  23141  resstopn  23151  hmpher  23749  nghmfval  24687  isnghm  24688  newval  27827  negsproplem2  28021  r1wf  35239  r1elcl  35241  cvmtop1  35442  cvmtop2  35443  imageval  36110  filnetlem4  36563  ismrc  43133  dnnumch3lem  43474  dnnumch3  43475  aomclem4  43485  grur1cld  44659  gricrel  48395  grlicrel  48482  fonex  49342  cicrcl2  49518  cic1st2nd  49522  oppfrcl  49603  eloppf  49608  initopropdlemlem  49714  initopropd  49718  termopropd  49719  zeroopropd  49720  reldmxpc  49721  reldmlan2  50092  reldmran2  50093  lanrcl  50096  ranrcl  50097