Theorem fndmi 6646

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5666   Fn wfn 6538

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 6546

This theorem is used by:  dmmpti  6686  dmmpo  8077  tfr2  8394  tz7.44-2  8403  rdgsuc  8420  tz7.48-2  8438  tz7.48-1  8439  tz7.48-3  8440  tz7.49  8441  brwitnlem  8501  om0x  8513  naddcllem  8671  naddov2  8674  naddasslem1  8690  naddasslem2  8691  elpmi  8852  elmapex  8854  pmresg  8877  pmsspw  8884  r1suc  9752  r1ord  9762  r1ord3  9764  onwf  9812  r1val3  9820  r1pw  9827  rankr1b  9846  alephcard  10073  alephnbtwn  10074  alephgeom  10085  dfac12lem2  10147  alephsing  10278  hsmexlem6  10433  zorn2lem4  10501  alephadd  10580  alephreg  10585  pwcfsdom  10586  r1limwun  10739  r1wunlim  10740  rankcf  10780  inatsk  10781  r1tskina  10785  dmaddpi  10893  dmmulpi  10894  seqexw  14073  hashkf  14388  bpolylem  16127  0rest  17507  firest  17510  homfeqbas  17777  cidpropd  17791  2oppchomf  17805  fucbas  18045  fuchom  18046  xpccofval  18263  oppchofcl  18341  oyoncl  18351  ex-chn2  18719  mulgfval  19166  gicer  19378  psgneldm  19604  psgneldm2  19605  psgnval  19608  ricrel  20629  psgnghm  21767  psgnghm2  21768  cldrcl  23220  iscldtop  23289  restrcl  23351  ssrest  23370  resstopn  23380  hmpher  23978  nghmfval  24916  isnghm  24917  bdaydm  27979  newval  28065  negsproplem2  28259  r1wf  35514  r1elcl  35516  onrankid  35519  rankfo  35530  cvmtop1  35773  cvmtop2  35774  imageval  36441  filnetlem4  36933  ismrc  43473  dnnumch3lem  43814  dnnumch3  43815  aomclem4  43825  grur1cld  44997  gricrel  48725  grlicrel  48812  fonex  49686  cicrcl2  49862  cic1st2nd  49866  oppfrcl  49947  eloppf  49952  initopropdlemlem  50058  initopropd  50062  termopropd  50063  zeroopropd  50064  reldmxpc  50065  reldmlan2  50436  reldmran2  50437  lanrcl  50440  ranrcl  50441