Theorem fndmi 6625

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

Syntax hints:   = wceq 1540  dom cdm 5641   Fn wfn 6509

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 6517

This theorem is referenced by:  dmmpti  6665  dmmpo  8053  tfr2  8369  tz7.44-2  8378  rdgsuc  8395  tz7.48-2  8413  tz7.48-1  8414  tz7.48-3  8415  tz7.49  8416  brwitnlem  8474  om0x  8486  naddcllem  8643  naddov2  8646  naddasslem1  8661  naddasslem2  8662  elpmi  8822  elmapex  8824  pmresg  8846  pmsspw  8853  r1suc  9730  r1ord  9740  r1ord3  9742  onwf  9790  r1val3  9798  r1pw  9805  rankr1b  9824  alephcard  10030  alephnbtwn  10031  alephgeom  10042  dfac12lem2  10105  alephsing  10236  hsmexlem6  10391  zorn2lem4  10459  alephadd  10537  alephreg  10542  pwcfsdom  10543  r1limwun  10696  r1wunlim  10697  rankcf  10737  inatsk  10738  r1tskina  10742  dmaddpi  10850  dmmulpi  10851  seqexw  13989  hashkf  14304  bpolylem  16021  0rest  17399  firest  17402  homfeqbas  17664  cidpropd  17678  2oppchomf  17692  fucbas  17932  fuchom  17933  xpccofval  18150  oppchofcl  18228  oyoncl  18238  mulgfval  19008  gicer  19216  psgneldm  19440  psgneldm2  19441  psgnval  19444  psgnghm  21496  psgnghm2  21497  cldrcl  22920  iscldtop  22989  restrcl  23051  ssrest  23070  resstopn  23080  hmpher  23678  nghmfval  24617  isnghm  24618  newval  27770  negsproplem2  27942  cvmtop1  35254  cvmtop2  35255  imageval  35925  filnetlem4  36376  ismrc  42696  dnnumch3lem  43042  dnnumch3  43043  aomclem4  43053  grur1cld  44228  gricrel  47923  grlicrel  48002  fonex  48859  cicrcl2  49036  cic1st2nd  49040  oppfrcl  49121  eloppf  49126  initopropdlemlem  49232  initopropd  49236  termopropd  49237  zeroopropd  49238  reldmxpc  49239  reldmlan2  49610  reldmran2  49611  lanrcl  49614  ranrcl  49615