Theorem fndmi 6641

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

Syntax hints:   = wceq 1570  dom cdm 5663   Fn wfn 6533

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 210  df-an 401  df-fn 6541

This theorem is referenced by:  dmmpti  6681  dmmpo  8069  tfr2  8386  tz7.44-2  8395  rdgsuc  8412  tz7.48-2  8430  tz7.48-1  8431  tz7.48-3  8432  tz7.49  8433  brwitnlem  8493  om0x  8505  naddcllem  8663  naddov2  8666  naddasslem1  8682  naddasslem2  8683  elpmi  8844  elmapex  8846  pmresg  8869  pmsspw  8876  r1suc  9743  r1ord  9753  r1ord3  9755  onwf  9803  r1val3  9811  r1pw  9818  rankr1b  9837  alephcard  10055  alephnbtwn  10056  alephgeom  10067  dfac12lem2  10129  alephsing  10261  hsmexlem6  10416  zorn2lem4  10484  alephadd  10563  alephreg  10568  pwcfsdom  10569  r1limwun  10722  r1wunlim  10723  rankcf  10763  inatsk  10764  r1tskina  10768  dmaddpi  10876  dmmulpi  10877  seqexw  14055  hashkf  14370  bpolylem  16103  0rest  17483  firest  17486  homfeqbas  17753  cidpropd  17767  2oppchomf  17781  fucbas  18021  fuchom  18022  xpccofval  18239  oppchofcl  18317  oyoncl  18327  ex-chn2  18695  mulgfval  19136  gicer  19348  psgneldm  19574  psgneldm2  19575  psgnval  19578  psgnghm  21711  psgnghm2  21712  cldrcl  23164  iscldtop  23233  restrcl  23295  ssrest  23314  resstopn  23324  hmpher  23922  nghmfval  24860  isnghm  24861  bdaydm  27920  newval  28006  negsproplem2  28200  r1wf  35467  r1elcl  35469  onrankid  35472  rankfo  35483  cvmtop1  35730  cvmtop2  35731  imageval  36398  filnetlem4  36870  ismrc  43412  dnnumch3lem  43753  dnnumch3  43754  aomclem4  43764  grur1cld  44936  gricrel  48661  grlicrel  48748  fonex  49622  cicrcl2  49798  cic1st2nd  49802  oppfrcl  49883  eloppf  49888  initopropdlemlem  49994  initopropd  49998  termopropd  49999  zeroopropd  50000  reldmxpc  50001  reldmlan2  50372  reldmran2  50373  lanrcl  50376  ranrcl  50377