Theorem fndmi 6635

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5651   Fn wfn 6526

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6534

This theorem is used by:  dmmpti  6675  dmmpo  8071  tfr2  8390  tz7.44-2  8399  rdgsuc  8416  tz7.48-2  8436  tz7.48-1  8437  tz7.48-3  8438  tz7.49  8439  brwitnlem  8499  om0x  8511  naddcllem  8669  naddov2  8672  naddasslem1  8688  naddasslem2  8689  elpmi  8850  elmapex  8852  pmresg  8882  pmsspw  8889  r1suc  9760  r1ord  9770  r1ord3  9772  onwf  9821  r1wf  9822  r1val3  9831  r1pw  9840  rankr1b  9862  alephcard  10130  alephnbtwn  10131  alephgeom  10142  dfac12lem2  10204  alephsing  10335  hsmexlem6  10490  zorn2lem4  10558  alephadd  10643  alephreg  10648  pwcfsdom  10649  r1limwun  10802  r1wunlim  10803  rankcf  10843  inatsk  10844  r1tskina  10848  dmaddpi  10956  dmmulpi  10957  seqexw  14140  hashkf  14456  bpolylem  16194  0rest  17580  firest  17583  homfeqbas  17850  cidpropd  17864  2oppchomf  17878  fucbas  18118  fuchom  18119  xpccofval  18336  oppchofcl  18414  oyoncl  18424  ex-chn2  18792  mulgfval  19259  gicer  19471  psgneldm  19697  psgneldm2  19698  psgnval  19701  ricrel  20724  psgnghm  21866  psgnghm2  21867  cldrcl  23324  iscldtop  23393  restrcl  23455  ssrest  23474  resstopn  23484  hmpher  24083  nghmfval  25021  isnghm  25022  bdaydm  28117  newval  28203  negsproplem2  28397  onrankid  35706  rankfo  35714  cvmtop1  35994  cvmtop2  35995  imageval  36662  rankeq1o  36902  hfninf  36905  filnetlem4  37139  ismrc  43665  dnnumch3lem  44006  dnnumch3  44007  aomclem4  44017  grur1cld  45189  gricrel  48961  grlicrel  49048  fonex  49921  cicrcl2  50095  cic1st2nd  50099  oppfrcl  50180  eloppf  50185  initopropdlemlem  50291  initopropd  50295  termopropd  50296  zeroopropd  50297  reldmxpc  50298  reldmlan2  50669  reldmran2  50670  lanrcl  50673  ranrcl  50674