Theorem fndmi 6683

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

Syntax hints:   = wceq 1537  dom cdm 5700   Fn wfn 6568

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 6576

This theorem is referenced by:  dmmpti  6724  dmmpo  8112  tfr2  8454  tz7.44-2  8463  rdgsuc  8480  tz7.48-2  8498  tz7.48-1  8499  tz7.48-3  8500  tz7.49  8501  brwitnlem  8563  om0x  8575  naddcllem  8732  naddov2  8735  naddasslem1  8750  naddasslem2  8751  elpmi  8904  elmapex  8906  pmresg  8928  pmsspw  8935  r1suc  9839  r1ord  9849  r1ord3  9851  onwf  9899  r1val3  9907  r1pw  9914  rankr1b  9933  alephcard  10139  alephnbtwn  10140  alephgeom  10151  dfac12lem2  10214  alephsing  10345  hsmexlem6  10500  zorn2lem4  10568  alephadd  10646  alephreg  10651  pwcfsdom  10652  r1limwun  10805  r1wunlim  10806  rankcf  10846  inatsk  10847  r1tskina  10851  dmaddpi  10959  dmmulpi  10960  seqexw  14068  hashkf  14381  bpolylem  16096  0rest  17489  firest  17492  homfeqbas  17754  cidpropd  17768  2oppchomf  17784  fucbas  18029  fuchom  18030  fuchomOLD  18031  xpccofval  18251  oppchofcl  18330  oyoncl  18340  mulgfval  19109  gicer  19317  psgneldm  19545  psgneldm2  19546  psgnval  19549  psgnghm  21621  psgnghm2  21622  cldrcl  23055  iscldtop  23124  restrcl  23186  ssrest  23205  resstopn  23215  hmpher  23813  nghmfval  24764  isnghm  24765  newval  27912  negsproplem2  28079  cvmtop1  35228  cvmtop2  35229  imageval  35894  filnetlem4  36347  ismrc  42657  dnnumch3lem  43003  dnnumch3  43004  aomclem4  43014  grur1cld  44201  gricrel  47772  grlicrel  47823