Theorem fndmi 6624

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

Syntax hints:   = wceq 1540  dom cdm 5640   Fn wfn 6508

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 6516

This theorem is referenced by:  dmmpti  6664  dmmpo  8052  tfr2  8368  tz7.44-2  8377  rdgsuc  8394  tz7.48-2  8412  tz7.48-1  8413  tz7.48-3  8414  tz7.49  8415  brwitnlem  8473  om0x  8485  naddcllem  8642  naddov2  8645  naddasslem1  8660  naddasslem2  8661  elpmi  8821  elmapex  8823  pmresg  8845  pmsspw  8852  r1suc  9729  r1ord  9739  r1ord3  9741  onwf  9789  r1val3  9797  r1pw  9804  rankr1b  9823  alephcard  10029  alephnbtwn  10030  alephgeom  10041  dfac12lem2  10104  alephsing  10235  hsmexlem6  10390  zorn2lem4  10458  alephadd  10536  alephreg  10541  pwcfsdom  10542  r1limwun  10695  r1wunlim  10696  rankcf  10736  inatsk  10737  r1tskina  10741  dmaddpi  10849  dmmulpi  10850  seqexw  13988  hashkf  14303  bpolylem  16020  0rest  17398  firest  17401  homfeqbas  17663  cidpropd  17677  2oppchomf  17691  fucbas  17931  fuchom  17932  xpccofval  18149  oppchofcl  18227  oyoncl  18237  mulgfval  19007  gicer  19215  psgneldm  19439  psgneldm2  19440  psgnval  19443  psgnghm  21495  psgnghm2  21496  cldrcl  22919  iscldtop  22988  restrcl  23050  ssrest  23069  resstopn  23079  hmpher  23677  nghmfval  24616  isnghm  24617  newval  27769  negsproplem2  27941  cvmtop1  35247  cvmtop2  35248  imageval  35913  filnetlem4  36364  ismrc  42682  dnnumch3lem  43028  dnnumch3  43029  aomclem4  43039  grur1cld  44214  gricrel  47909  grlicrel  47988  fonex  48845  cicrcl2  49022  cic1st2nd  49026  oppfrcl  49107  eloppf  49112  initopropdlemlem  49218  initopropd  49222  termopropd  49223  zeroopropd  49224  reldmxpc  49225  reldmlan2  49596  reldmran2  49597  lanrcl  49600  ranrcl  49601