Theorem fndmi 6640

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

Syntax hints:   = wceq 1567  dom cdm 5662   Fn wfn 6532

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 210  df-an 401  df-fn 6540

This theorem is referenced by:  dmmpti  6680  dmmpo  8067  tfr2  8384  tz7.44-2  8393  rdgsuc  8410  tz7.48-2  8428  tz7.48-1  8429  tz7.48-3  8430  tz7.49  8431  brwitnlem  8491  om0x  8503  naddcllem  8661  naddov2  8664  naddasslem1  8680  naddasslem2  8681  elpmi  8842  elmapex  8844  pmresg  8867  pmsspw  8874  r1suc  9741  r1ord  9751  r1ord3  9753  onwf  9801  r1val3  9809  r1pw  9816  rankr1b  9835  alephcard  10053  alephnbtwn  10054  alephgeom  10065  dfac12lem2  10127  alephsing  10259  hsmexlem6  10414  zorn2lem4  10482  alephadd  10561  alephreg  10566  pwcfsdom  10567  r1limwun  10720  r1wunlim  10721  rankcf  10761  inatsk  10762  r1tskina  10766  dmaddpi  10874  dmmulpi  10875  seqexw  14052  hashkf  14367  bpolylem  16101  0rest  17481  firest  17484  homfeqbas  17751  cidpropd  17765  2oppchomf  17779  fucbas  18019  fuchom  18020  xpccofval  18237  oppchofcl  18315  oyoncl  18325  ex-chn2  18693  mulgfval  19134  gicer  19346  psgneldm  19572  psgneldm2  19573  psgnval  19576  psgnghm  21698  psgnghm2  21699  cldrcl  23151  iscldtop  23220  restrcl  23282  ssrest  23301  resstopn  23311  hmpher  23909  nghmfval  24847  isnghm  24848  bdaydm  27907  newval  27993  negsproplem2  28187  r1wf  35431  r1elcl  35433  cvmtop1  35650  cvmtop2  35651  imageval  36318  filnetlem4  36780  ismrc  43323  dnnumch3lem  43664  dnnumch3  43665  aomclem4  43675  grur1cld  44847  gricrel  48572  grlicrel  48659  fonex  49529  cicrcl2  49705  cic1st2nd  49709  oppfrcl  49790  eloppf  49795  initopropdlemlem  49901  initopropd  49905  termopropd  49906  zeroopropd  49907  reldmxpc  49908  reldmlan2  50279  reldmran2  50280  lanrcl  50283  ranrcl  50284