Theorem fndmi 6590

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

Syntax hints:   = wceq 1540  dom cdm 5623   Fn wfn 6481

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 6489

This theorem is referenced by:  dmmpti  6630  dmmpo  8013  tfr2  8327  tz7.44-2  8336  rdgsuc  8353  tz7.48-2  8371  tz7.48-1  8372  tz7.48-3  8373  tz7.49  8374  brwitnlem  8432  om0x  8444  naddcllem  8601  naddov2  8604  naddasslem1  8619  naddasslem2  8620  elpmi  8780  elmapex  8782  pmresg  8804  pmsspw  8811  r1suc  9685  r1ord  9695  r1ord3  9697  onwf  9745  r1val3  9753  r1pw  9760  rankr1b  9779  alephcard  9983  alephnbtwn  9984  alephgeom  9995  dfac12lem2  10058  alephsing  10189  hsmexlem6  10344  zorn2lem4  10412  alephadd  10490  alephreg  10495  pwcfsdom  10496  r1limwun  10649  r1wunlim  10650  rankcf  10690  inatsk  10691  r1tskina  10695  dmaddpi  10803  dmmulpi  10804  seqexw  13942  hashkf  14257  bpolylem  15973  0rest  17351  firest  17354  homfeqbas  17620  cidpropd  17634  2oppchomf  17648  fucbas  17888  fuchom  17889  xpccofval  18106  oppchofcl  18184  oyoncl  18194  mulgfval  18966  gicer  19174  psgneldm  19400  psgneldm2  19401  psgnval  19404  psgnghm  21505  psgnghm2  21506  cldrcl  22929  iscldtop  22998  restrcl  23060  ssrest  23079  resstopn  23089  hmpher  23687  nghmfval  24626  isnghm  24627  newval  27783  negsproplem2  27958  cvmtop1  35232  cvmtop2  35233  imageval  35903  filnetlem4  36354  ismrc  42674  dnnumch3lem  43019  dnnumch3  43020  aomclem4  43030  grur1cld  44205  gricrel  47904  grlicrel  47991  fonex  48852  cicrcl2  49029  cic1st2nd  49033  oppfrcl  49114  eloppf  49119  initopropdlemlem  49225  initopropd  49229  termopropd  49230  zeroopropd  49231  reldmxpc  49232  reldmlan2  49603  reldmran2  49604  lanrcl  49607  ranrcl  49608