Theorem fndmi 6642

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

Syntax hints:   = wceq 1540  dom cdm 5654   Fn wfn 6526

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 6534

This theorem is referenced by:  dmmpti  6682  dmmpo  8070  tfr2  8412  tz7.44-2  8421  rdgsuc  8438  tz7.48-2  8456  tz7.48-1  8457  tz7.48-3  8458  tz7.49  8459  brwitnlem  8519  om0x  8531  naddcllem  8688  naddov2  8691  naddasslem1  8706  naddasslem2  8707  elpmi  8860  elmapex  8862  pmresg  8884  pmsspw  8891  r1suc  9784  r1ord  9794  r1ord3  9796  onwf  9844  r1val3  9852  r1pw  9859  rankr1b  9878  alephcard  10084  alephnbtwn  10085  alephgeom  10096  dfac12lem2  10159  alephsing  10290  hsmexlem6  10445  zorn2lem4  10513  alephadd  10591  alephreg  10596  pwcfsdom  10597  r1limwun  10750  r1wunlim  10751  rankcf  10791  inatsk  10792  r1tskina  10796  dmaddpi  10904  dmmulpi  10905  seqexw  14035  hashkf  14350  bpolylem  16064  0rest  17443  firest  17446  homfeqbas  17708  cidpropd  17722  2oppchomf  17736  fucbas  17976  fuchom  17977  xpccofval  18194  oppchofcl  18272  oyoncl  18282  mulgfval  19052  gicer  19260  psgneldm  19484  psgneldm2  19485  psgnval  19488  psgnghm  21540  psgnghm2  21541  cldrcl  22964  iscldtop  23033  restrcl  23095  ssrest  23114  resstopn  23124  hmpher  23722  nghmfval  24661  isnghm  24662  newval  27815  negsproplem2  27987  cvmtop1  35282  cvmtop2  35283  imageval  35948  filnetlem4  36399  ismrc  42724  dnnumch3lem  43070  dnnumch3  43071  aomclem4  43081  grur1cld  44256  gricrel  47932  grlicrel  48011  fonex  48842  cicrcl2  49010  cic1st2nd  49014  initopropdlemlem  49156  initopropd  49160  termopropd  49161  zeroopropd  49162  reldmxpc  49163  reldmlan2  49492  reldmran2  49493  lanrcl  49496  ranrcl  49497