Theorem fndmi 6596

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

Syntax hints:   = wceq 1541  dom cdm 5624   Fn wfn 6487

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 6495

This theorem is referenced by:  dmmpti  6636  dmmpo  8015  tfr2  8329  tz7.44-2  8338  rdgsuc  8355  tz7.48-2  8373  tz7.48-1  8374  tz7.48-3  8375  tz7.49  8376  brwitnlem  8434  om0x  8446  naddcllem  8604  naddov2  8607  naddasslem1  8622  naddasslem2  8623  elpmi  8783  elmapex  8785  pmresg  8808  pmsspw  8815  r1suc  9682  r1ord  9692  r1ord3  9694  onwf  9742  r1val3  9750  r1pw  9757  rankr1b  9776  alephcard  9980  alephnbtwn  9981  alephgeom  9992  dfac12lem2  10055  alephsing  10186  hsmexlem6  10341  zorn2lem4  10409  alephadd  10488  alephreg  10493  pwcfsdom  10494  r1limwun  10647  r1wunlim  10648  rankcf  10688  inatsk  10689  r1tskina  10693  dmaddpi  10801  dmmulpi  10802  seqexw  13940  hashkf  14255  bpolylem  15971  0rest  17349  firest  17352  homfeqbas  17619  cidpropd  17633  2oppchomf  17647  fucbas  17887  fuchom  17888  xpccofval  18105  oppchofcl  18183  oyoncl  18193  ex-chn2  18561  mulgfval  18999  gicer  19206  psgneldm  19432  psgneldm2  19433  psgnval  19436  psgnghm  21535  psgnghm2  21536  cldrcl  22970  iscldtop  23039  restrcl  23101  ssrest  23120  resstopn  23130  hmpher  23728  nghmfval  24666  isnghm  24667  newval  27831  negsproplem2  28025  r1wf  35252  r1elcl  35254  cvmtop1  35454  cvmtop2  35455  imageval  36122  filnetlem4  36575  ismrc  42939  dnnumch3lem  43284  dnnumch3  43285  aomclem4  43295  grur1cld  44469  gricrel  48161  grlicrel  48248  fonex  49108  cicrcl2  49284  cic1st2nd  49288  oppfrcl  49369  eloppf  49374  initopropdlemlem  49480  initopropd  49484  termopropd  49485  zeroopropd  49486  reldmxpc  49487  reldmlan2  49858  reldmran2  49859  lanrcl  49862  ranrcl  49863