Theorem fndmi 6521

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

Syntax hints:   = wceq 1539  dom cdm 5580   Fn wfn 6413

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 206  df-an 396  df-fn 6421

This theorem is referenced by:  dmmpti  6561  dmmpo  7884  tfr2  8200  tz7.44-2  8209  rdgsuc  8226  tz7.48-2  8243  tz7.48-1  8244  tz7.48-3  8245  tz7.49  8246  brwitnlem  8299  om0x  8311  elpmi  8592  elmapex  8594  pmresg  8616  pmsspw  8623  r1suc  9459  r1ord  9469  r1ord3  9471  onwf  9519  r1val3  9527  r1pw  9534  rankr1b  9553  alephcard  9757  alephnbtwn  9758  alephgeom  9769  dfac12lem2  9831  alephsing  9963  hsmexlem6  10118  zorn2lem4  10186  alephadd  10264  alephreg  10269  pwcfsdom  10270  r1limwun  10423  r1wunlim  10424  rankcf  10464  inatsk  10465  r1tskina  10469  dmaddpi  10577  dmmulpi  10578  seqexw  13665  hashkf  13974  bpolylem  15686  0rest  17057  firest  17060  homfeqbas  17322  cidpropd  17336  2oppchomf  17352  fucbas  17593  fuchom  17594  fuchomOLD  17595  xpccofval  17815  oppchofcl  17894  oyoncl  17904  mulgfval  18617  gicer  18807  psgneldm  19026  psgneldm2  19027  psgnval  19030  psgnghm  20697  psgnghm2  20698  cldrcl  22085  iscldtop  22154  restrcl  22216  ssrest  22235  resstopn  22245  hmpher  22843  nghmfval  23792  isnghm  23793  cvmtop1  33122  cvmtop2  33123  naddcllem  33758  naddov2  33761  newval  33966  imageval  34159  filnetlem4  34497  ismrc  40439  dnnumch3lem  40787  dnnumch3  40788  aomclem4  40798  grur1cld  41739