Theorem fndmi 6590

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 6589	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1541  dom cdm 5619   Fn wfn 6481

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 6489

This theorem is referenced by:  dmmpti  6630  dmmpo  8009  tfr2  8323  tz7.44-2  8332  rdgsuc  8349  tz7.48-2  8367  tz7.48-1  8368  tz7.48-3  8369  tz7.49  8370  brwitnlem  8428  om0x  8440  naddcllem  8597  naddov2  8600  naddasslem1  8615  naddasslem2  8616  elpmi  8776  elmapex  8778  pmresg  8800  pmsspw  8807  r1suc  9670  r1ord  9680  r1ord3  9682  onwf  9730  r1val3  9738  r1pw  9745  rankr1b  9764  alephcard  9968  alephnbtwn  9969  alephgeom  9980  dfac12lem2  10043  alephsing  10174  hsmexlem6  10329  zorn2lem4  10397  alephadd  10475  alephreg  10480  pwcfsdom  10481  r1limwun  10634  r1wunlim  10635  rankcf  10675  inatsk  10676  r1tskina  10680  dmaddpi  10788  dmmulpi  10789  seqexw  13926  hashkf  14241  bpolylem  15957  0rest  17335  firest  17338  homfeqbas  17604  cidpropd  17618  2oppchomf  17632  fucbas  17872  fuchom  17873  xpccofval  18090  oppchofcl  18168  oyoncl  18178  ex-chn2  18546  mulgfval  18984  gicer  19191  psgneldm  19417  psgneldm2  19418  psgnval  19421  psgnghm  21519  psgnghm2  21520  cldrcl  22942  iscldtop  23011  restrcl  23073  ssrest  23092  resstopn  23102  hmpher  23700  nghmfval  24638  isnghm  24639  newval  27797  negsproplem2  27972  r1wf  35128  r1elcl  35130  cvmtop1  35325  cvmtop2  35326  imageval  35993  filnetlem4  36446  ismrc  42818  dnnumch3lem  43163  dnnumch3  43164  aomclem4  43174  grur1cld  44349  gricrel  48043  grlicrel  48130  fonex  48991  cicrcl2  49168  cic1st2nd  49172  oppfrcl  49253  eloppf  49258  initopropdlemlem  49364  initopropd  49368  termopropd  49369  zeroopropd  49370  reldmxpc  49371  reldmlan2  49742  reldmran2  49743  lanrcl  49746  ranrcl  49747