Theorem fndmi 6643

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

This proof depends on syntax axioms:   = wceq 1569  dom cdm 5650   Fn wfn 6533

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 6541

This theorem is used by:  dmmpti  6683  dmmpo  8082  tfr2  8409  tz7.44-2  8418  rdgsuc  8435  tz7.48-2  8455  tz7.48-1  8456  tz7.48-3  8457  tz7.49  8458  brwitnlem  8518  om0x  8530  naddcllem  8688  naddov2  8691  naddasslem1  8707  naddasslem2  8708  elpmi  8869  elmapex  8871  pmresg  8901  pmsspw  8908  r1suc  9780  r1lim  9782  r1ord  9790  r1ord3  9792  onwf  9843  r1wf  9844  r1val3  9853  r1pw  9862  rankr1b  9884  alephcard  10152  alephnbtwn  10153  alephgeom  10164  dfac12lem2  10226  alephsing  10357  hsmexlem6  10512  zorn2lem4  10580  alephadd  10665  alephreg  10670  pwcfsdom  10671  r1limwun  10824  r1wunlim  10825  rankcf  10865  inatsk  10866  r1tskina  10870  dmaddpi  10978  dmmulpi  10979  seqexw  14163  hashkf  14479  bpolylem  16219  0rest  17605  firest  17608  homfeqbas  17875  cidpropd  17889  2oppchomf  17903  fucbas  18143  fuchom  18144  xpccofval  18361  oppchofcl  18439  oyoncl  18449  ex-chn2  18817  mulgfval  19284  gicer  19496  psgneldm  19722  psgneldm2  19723  psgnval  19726  ricrel  20749  psgnghm  21891  psgnghm2  21892  cldrcl  23349  iscldtop  23418  restrcl  23480  ssrest  23499  resstopn  23509  hmpher  24108  nghmfval  25046  isnghm  25047  bdaydm  28140  newval  28226  negsproplem2  28420  onrankid  35779  rankfo  35787  acwer1prclem  35815  acwer1prc  35816  j0ltaleph  35947  cvmtop1  36111  cvmtop2  36112  imageval  36784  rankeq1o  37024  hfninf  37027  filnetlem4  37261  ismrc  43805  dnnumch3lem  44146  dnnumch3  44147  aomclem4  44152  grur1cld  45323  gricrel  49110  grlicrel  49197  fonex  50071  cicrcl2  50250  cic1st2nd  50254  oppfrcl  50337  eloppf  50342  initopropdlemlem  50454  initopropd  50458  termopropd  50459  zeroopropd  50460  reldmxpc  50461  reldmlan2  50893  reldmran2  50894  lanrcl  50897  ranrcl  50898