Theorem fndmi 6673

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

Syntax hints:   = wceq 1537  dom cdm 5689   Fn wfn 6558

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 6566

This theorem is referenced by:  dmmpti  6713  dmmpo  8095  tfr2  8437  tz7.44-2  8446  rdgsuc  8463  tz7.48-2  8481  tz7.48-1  8482  tz7.48-3  8483  tz7.49  8484  brwitnlem  8544  om0x  8556  naddcllem  8713  naddov2  8716  naddasslem1  8731  naddasslem2  8732  elpmi  8885  elmapex  8887  pmresg  8909  pmsspw  8916  r1suc  9808  r1ord  9818  r1ord3  9820  onwf  9868  r1val3  9876  r1pw  9883  rankr1b  9902  alephcard  10108  alephnbtwn  10109  alephgeom  10120  dfac12lem2  10183  alephsing  10314  hsmexlem6  10469  zorn2lem4  10537  alephadd  10615  alephreg  10620  pwcfsdom  10621  r1limwun  10774  r1wunlim  10775  rankcf  10815  inatsk  10816  r1tskina  10820  dmaddpi  10928  dmmulpi  10929  seqexw  14055  hashkf  14368  bpolylem  16081  0rest  17476  firest  17479  homfeqbas  17741  cidpropd  17755  2oppchomf  17771  fucbas  18016  fuchom  18017  fuchomOLD  18018  xpccofval  18238  oppchofcl  18317  oyoncl  18327  mulgfval  19100  gicer  19308  psgneldm  19536  psgneldm2  19537  psgnval  19540  psgnghm  21616  psgnghm2  21617  cldrcl  23050  iscldtop  23119  restrcl  23181  ssrest  23200  resstopn  23210  hmpher  23808  nghmfval  24759  isnghm  24760  newval  27909  negsproplem2  28076  cvmtop1  35245  cvmtop2  35246  imageval  35912  filnetlem4  36364  ismrc  42689  dnnumch3lem  43035  dnnumch3  43036  aomclem4  43046  grur1cld  44228  gricrel  47826  grlicrel  47902