Theorem fndmi 6585

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

Syntax hints:   = wceq 1541  dom cdm 5616   Fn wfn 6476

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 6484

This theorem is referenced by:  dmmpti  6625  dmmpo  8003  tfr2  8317  tz7.44-2  8326  rdgsuc  8343  tz7.48-2  8361  tz7.48-1  8362  tz7.48-3  8363  tz7.49  8364  brwitnlem  8422  om0x  8434  naddcllem  8591  naddov2  8594  naddasslem1  8609  naddasslem2  8610  elpmi  8770  elmapex  8772  pmresg  8794  pmsspw  8801  r1suc  9660  r1ord  9670  r1ord3  9672  onwf  9720  r1val3  9728  r1pw  9735  rankr1b  9754  alephcard  9958  alephnbtwn  9959  alephgeom  9970  dfac12lem2  10033  alephsing  10164  hsmexlem6  10319  zorn2lem4  10387  alephadd  10465  alephreg  10470  pwcfsdom  10471  r1limwun  10624  r1wunlim  10625  rankcf  10665  inatsk  10666  r1tskina  10670  dmaddpi  10778  dmmulpi  10779  seqexw  13921  hashkf  14236  bpolylem  15952  0rest  17330  firest  17333  homfeqbas  17599  cidpropd  17613  2oppchomf  17627  fucbas  17867  fuchom  17868  xpccofval  18085  oppchofcl  18163  oyoncl  18173  ex-chn2  18541  mulgfval  18979  gicer  19187  psgneldm  19413  psgneldm2  19414  psgnval  19417  psgnghm  21515  psgnghm2  21516  cldrcl  22939  iscldtop  23008  restrcl  23070  ssrest  23089  resstopn  23099  hmpher  23697  nghmfval  24635  isnghm  24636  newval  27794  negsproplem2  27969  r1wf  35100  r1elcl  35102  cvmtop1  35292  cvmtop2  35293  imageval  35963  filnetlem4  36414  ismrc  42733  dnnumch3lem  43078  dnnumch3  43079  aomclem4  43089  grur1cld  44264  gricrel  47949  grlicrel  48036  fonex  48897  cicrcl2  49074  cic1st2nd  49078  oppfrcl  49159  eloppf  49164  initopropdlemlem  49270  initopropd  49274  termopropd  49275  zeroopropd  49276  reldmxpc  49277  reldmlan2  49648  reldmran2  49649  lanrcl  49652  ranrcl  49653