Theorem fndmi 6672

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

Syntax hints:   = wceq 1540  dom cdm 5685   Fn wfn 6556

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 6564

This theorem is referenced by:  dmmpti  6712  dmmpo  8096  tfr2  8438  tz7.44-2  8447  rdgsuc  8464  tz7.48-2  8482  tz7.48-1  8483  tz7.48-3  8484  tz7.49  8485  brwitnlem  8545  om0x  8557  naddcllem  8714  naddov2  8717  naddasslem1  8732  naddasslem2  8733  elpmi  8886  elmapex  8888  pmresg  8910  pmsspw  8917  r1suc  9810  r1ord  9820  r1ord3  9822  onwf  9870  r1val3  9878  r1pw  9885  rankr1b  9904  alephcard  10110  alephnbtwn  10111  alephgeom  10122  dfac12lem2  10185  alephsing  10316  hsmexlem6  10471  zorn2lem4  10539  alephadd  10617  alephreg  10622  pwcfsdom  10623  r1limwun  10776  r1wunlim  10777  rankcf  10817  inatsk  10818  r1tskina  10822  dmaddpi  10930  dmmulpi  10931  seqexw  14058  hashkf  14371  bpolylem  16084  0rest  17474  firest  17477  homfeqbas  17739  cidpropd  17753  2oppchomf  17767  fucbas  18008  fuchom  18009  xpccofval  18227  oppchofcl  18305  oyoncl  18315  mulgfval  19087  gicer  19295  psgneldm  19521  psgneldm2  19522  psgnval  19525  psgnghm  21598  psgnghm2  21599  cldrcl  23034  iscldtop  23103  restrcl  23165  ssrest  23184  resstopn  23194  hmpher  23792  nghmfval  24743  isnghm  24744  newval  27894  negsproplem2  28061  cvmtop1  35265  cvmtop2  35266  imageval  35931  filnetlem4  36382  ismrc  42712  dnnumch3lem  43058  dnnumch3  43059  aomclem4  43069  grur1cld  44251  gricrel  47888  grlicrel  47966  reldmxpc  48952