Theorem fndmi 6622

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

Syntax hints:   = wceq 1540  dom cdm 5638   Fn wfn 6506

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 6514

This theorem is referenced by:  dmmpti  6662  dmmpo  8050  tfr2  8366  tz7.44-2  8375  rdgsuc  8392  tz7.48-2  8410  tz7.48-1  8411  tz7.48-3  8412  tz7.49  8413  brwitnlem  8471  om0x  8483  naddcllem  8640  naddov2  8643  naddasslem1  8658  naddasslem2  8659  elpmi  8819  elmapex  8821  pmresg  8843  pmsspw  8850  r1suc  9723  r1ord  9733  r1ord3  9735  onwf  9783  r1val3  9791  r1pw  9798  rankr1b  9817  alephcard  10023  alephnbtwn  10024  alephgeom  10035  dfac12lem2  10098  alephsing  10229  hsmexlem6  10384  zorn2lem4  10452  alephadd  10530  alephreg  10535  pwcfsdom  10536  r1limwun  10689  r1wunlim  10690  rankcf  10730  inatsk  10731  r1tskina  10735  dmaddpi  10843  dmmulpi  10844  seqexw  13982  hashkf  14297  bpolylem  16014  0rest  17392  firest  17395  homfeqbas  17657  cidpropd  17671  2oppchomf  17685  fucbas  17925  fuchom  17926  xpccofval  18143  oppchofcl  18221  oyoncl  18231  mulgfval  19001  gicer  19209  psgneldm  19433  psgneldm2  19434  psgnval  19437  psgnghm  21489  psgnghm2  21490  cldrcl  22913  iscldtop  22982  restrcl  23044  ssrest  23063  resstopn  23073  hmpher  23671  nghmfval  24610  isnghm  24611  newval  27763  negsproplem2  27935  cvmtop1  35247  cvmtop2  35248  imageval  35918  filnetlem4  36369  ismrc  42689  dnnumch3lem  43035  dnnumch3  43036  aomclem4  43046  grur1cld  44221  gricrel  47919  grlicrel  47998  fonex  48855  cicrcl2  49032  cic1st2nd  49036  oppfrcl  49117  eloppf  49122  initopropdlemlem  49228  initopropd  49232  termopropd  49233  zeroopropd  49234  reldmxpc  49235  reldmlan2  49606  reldmran2  49607  lanrcl  49610  ranrcl  49611