Theorem fndmi 6640

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5659   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6540

This theorem is used by:  dmmpti  6680  dmmpo  8072  tfr2  8391  tz7.44-2  8400  rdgsuc  8417  tz7.48-2  8435  tz7.48-1  8436  tz7.48-3  8437  tz7.49  8438  brwitnlem  8498  om0x  8510  naddcllem  8668  naddov2  8671  naddasslem1  8687  naddasslem2  8688  elpmi  8849  elmapex  8851  pmresg  8881  pmsspw  8888  r1suc  9756  r1ord  9766  r1ord3  9768  onwf  9816  r1val3  9824  r1pw  9831  rankr1b  9850  alephcard  10077  alephnbtwn  10078  alephgeom  10089  dfac12lem2  10151  alephsing  10282  hsmexlem6  10437  zorn2lem4  10505  alephadd  10590  alephreg  10595  pwcfsdom  10596  r1limwun  10749  r1wunlim  10750  rankcf  10790  inatsk  10791  r1tskina  10795  dmaddpi  10903  dmmulpi  10904  seqexw  14085  hashkf  14400  bpolylem  16140  0rest  17520  firest  17523  homfeqbas  17790  cidpropd  17804  2oppchomf  17818  fucbas  18058  fuchom  18059  xpccofval  18276  oppchofcl  18354  oyoncl  18364  ex-chn2  18732  mulgfval  19198  gicer  19410  psgneldm  19636  psgneldm2  19637  psgnval  19640  ricrel  20661  psgnghm  21799  psgnghm2  21800  cldrcl  23257  iscldtop  23326  restrcl  23388  ssrest  23407  resstopn  23417  hmpher  24016  nghmfval  24954  isnghm  24955  bdaydm  28022  newval  28108  negsproplem2  28302  r1wf  35611  r1elcl  35613  onrankid  35616  rankfo  35627  cvmtop1  35847  cvmtop2  35848  imageval  36515  filnetlem4  37008  ismrc  43554  dnnumch3lem  43895  dnnumch3  43896  aomclem4  43906  grur1cld  45078  gricrel  48843  grlicrel  48930  fonex  49803  cicrcl2  49977  cic1st2nd  49981  oppfrcl  50062  eloppf  50067  initopropdlemlem  50173  initopropd  50177  termopropd  50178  zeroopropd  50179  reldmxpc  50180  reldmlan2  50551  reldmran2  50552  lanrcl  50555  ranrcl  50556