Theorem fndmi 6629

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

Syntax hints:   = wceq 1563  dom cdm 5652   Fn wfn 6520

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 6528

This theorem is referenced by:  dmmpti  6669  dmmpo  8056  tfr2  8373  tz7.44-2  8382  rdgsuc  8399  tz7.48-2  8417  tz7.48-1  8418  tz7.48-3  8419  tz7.49  8420  brwitnlem  8480  om0x  8492  naddcllem  8650  naddov2  8653  naddasslem1  8669  naddasslem2  8670  elpmi  8831  elmapex  8833  pmresg  8856  pmsspw  8863  r1suc  9730  r1ord  9740  r1ord3  9742  onwf  9790  r1val3  9798  r1pw  9805  rankr1b  9824  alephcard  10042  alephnbtwn  10043  alephgeom  10054  dfac12lem2  10116  alephsing  10248  hsmexlem6  10403  zorn2lem4  10471  alephadd  10550  alephreg  10555  pwcfsdom  10556  r1limwun  10709  r1wunlim  10710  rankcf  10750  inatsk  10751  r1tskina  10755  dmaddpi  10863  dmmulpi  10864  seqexw  14044  hashkf  14359  bpolylem  16092  0rest  17472  firest  17475  homfeqbas  17742  cidpropd  17756  2oppchomf  17770  fucbas  18010  fuchom  18011  xpccofval  18228  oppchofcl  18306  oyoncl  18316  ex-chn2  18684  mulgfval  19126  gicer  19338  psgneldm  19564  psgneldm2  19565  psgnval  19568  psgnghm  21690  psgnghm2  21691  cldrcl  23144  iscldtop  23213  restrcl  23275  ssrest  23294  resstopn  23304  hmpher  23902  nghmfval  24840  isnghm  24841  bdaydm  27900  newval  27986  negsproplem2  28180  r1wf  35404  r1elcl  35406  cvmtop1  35623  cvmtop2  35624  imageval  36291  filnetlem4  36754  ismrc  43294  dnnumch3lem  43635  dnnumch3  43636  aomclem4  43646  grur1cld  44820  gricrel  48539  grlicrel  48626  fonex  49496  cicrcl2  49672  cic1st2nd  49676  oppfrcl  49757  eloppf  49762  initopropdlemlem  49868  initopropd  49872  termopropd  49873  zeroopropd  49874  reldmxpc  49875  reldmlan2  50246  reldmran2  50247  lanrcl  50250  ranrcl  50251