Theorem fndmi 6604

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

Syntax hints:   = wceq 1542  dom cdm 5632   Fn wfn 6495

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 6503

This theorem is referenced by:  dmmpti  6644  dmmpo  8025  tfr2  8339  tz7.44-2  8348  rdgsuc  8365  tz7.48-2  8383  tz7.48-1  8384  tz7.48-3  8385  tz7.49  8386  brwitnlem  8444  om0x  8456  naddcllem  8614  naddov2  8617  naddasslem1  8632  naddasslem2  8633  elpmi  8795  elmapex  8797  pmresg  8820  pmsspw  8827  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  13952  hashkf  14267  bpolylem  15983  0rest  17361  firest  17364  homfeqbas  17631  cidpropd  17645  2oppchomf  17659  fucbas  17899  fuchom  17900  xpccofval  18117  oppchofcl  18195  oyoncl  18205  ex-chn2  18573  mulgfval  19011  gicer  19218  psgneldm  19444  psgneldm2  19445  psgnval  19448  psgnghm  21547  psgnghm2  21548  cldrcl  22982  iscldtop  23051  restrcl  23113  ssrest  23132  resstopn  23142  hmpher  23740  nghmfval  24678  isnghm  24679  newval  27843  negsproplem2  28037  r1wf  35271  r1elcl  35273  cvmtop1  35473  cvmtop2  35474  imageval  36141  filnetlem4  36594  ismrc  43052  dnnumch3lem  43397  dnnumch3  43398  aomclem4  43408  grur1cld  44582  gricrel  48273  grlicrel  48360  fonex  49220  cicrcl2  49396  cic1st2nd  49400  oppfrcl  49481  eloppf  49486  initopropdlemlem  49592  initopropd  49596  termopropd  49597  zeroopropd  49598  reldmxpc  49599  reldmlan2  49970  reldmran2  49971  lanrcl  49974  ranrcl  49975