Theorem fndmi 6596

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

Syntax hints:   = wceq 1547  dom cdm 5625   Fn wfn 6487

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 208  df-an 397  df-fn 6495

This theorem is referenced by:  dmmpti  6636  dmmpo  8020  tfr2  8334  tz7.44-2  8343  rdgsuc  8360  tz7.48-2  8378  tz7.48-1  8379  tz7.48-3  8380  tz7.49  8381  brwitnlem  8439  om0x  8451  naddcllem  8609  naddov2  8612  naddasslem1  8627  naddasslem2  8628  elpmi  8790  elmapex  8792  pmresg  8815  pmsspw  8822  r1suc  9692  r1ord  9702  r1ord3  9704  onwf  9752  r1val3  9760  r1pw  9767  rankr1b  9786  alephcard  9990  alephnbtwn  9991  alephgeom  10002  dfac12lem2  10065  alephsing  10196  hsmexlem6  10351  zorn2lem4  10419  alephadd  10498  alephreg  10503  pwcfsdom  10504  r1limwun  10657  r1wunlim  10658  rankcf  10698  inatsk  10699  r1tskina  10703  dmaddpi  10811  dmmulpi  10812  seqexw  13977  hashkf  14292  bpolylem  16011  0rest  17390  firest  17393  homfeqbas  17660  cidpropd  17674  2oppchomf  17688  fucbas  17928  fuchom  17929  xpccofval  18146  oppchofcl  18224  oyoncl  18234  ex-chn2  18602  mulgfval  19043  gicer  19250  psgneldm  19476  psgneldm2  19477  psgnval  19480  psgnghm  21562  psgnghm2  21563  cldrcl  23016  iscldtop  23085  restrcl  23147  ssrest  23166  resstopn  23176  hmpher  23774  nghmfval  24712  isnghm  24713  newval  27852  negsproplem2  28046  r1wf  35284  r1elcl  35286  cvmtop1  35495  cvmtop2  35496  imageval  36163  filnetlem4  36616  ismrc  43157  dnnumch3lem  43498  dnnumch3  43499  aomclem4  43509  grur1cld  44683  gricrel  48417  grlicrel  48504  fonex  49364  cicrcl2  49540  cic1st2nd  49544  oppfrcl  49625  eloppf  49630  initopropdlemlem  49736  initopropd  49740  termopropd  49741  zeroopropd  49742  reldmxpc  49743  reldmlan2  50114  reldmran2  50115  lanrcl  50118  ranrcl  50119