Theorem fndmi 6659

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

Syntax hints:   = wceq 1533  dom cdm 5678   Fn wfn 6544

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 206  df-an 395  df-fn 6552

This theorem is referenced by:  dmmpti  6700  dmmpo  8076  tfr2  8419  tz7.44-2  8428  rdgsuc  8445  tz7.48-2  8463  tz7.48-1  8464  tz7.48-3  8465  tz7.49  8466  brwitnlem  8528  om0x  8540  naddcllem  8697  naddov2  8700  naddasslem1  8715  naddasslem2  8716  elpmi  8865  elmapex  8867  pmresg  8889  pmsspw  8896  r1suc  9795  r1ord  9805  r1ord3  9807  onwf  9855  r1val3  9863  r1pw  9870  rankr1b  9889  alephcard  10095  alephnbtwn  10096  alephgeom  10107  dfac12lem2  10169  alephsing  10301  hsmexlem6  10456  zorn2lem4  10524  alephadd  10602  alephreg  10607  pwcfsdom  10608  r1limwun  10761  r1wunlim  10762  rankcf  10802  inatsk  10803  r1tskina  10807  dmaddpi  10915  dmmulpi  10916  seqexw  14018  hashkf  14327  bpolylem  16028  0rest  17414  firest  17417  homfeqbas  17679  cidpropd  17693  2oppchomf  17709  fucbas  17954  fuchom  17955  fuchomOLD  17956  xpccofval  18176  oppchofcl  18255  oyoncl  18265  mulgfval  19033  gicer  19240  psgneldm  19470  psgneldm2  19471  psgnval  19474  psgnghm  21529  psgnghm2  21530  cldrcl  22974  iscldtop  23043  restrcl  23105  ssrest  23124  resstopn  23134  hmpher  23732  nghmfval  24683  isnghm  24684  newval  27828  negsproplem2  27987  cvmtop1  34998  cvmtop2  34999  imageval  35654  filnetlem4  35993  ismrc  42260  dnnumch3lem  42609  dnnumch3  42610  aomclem4  42620  grur1cld  43808  gricrel  47368