Theorem fndmi 6621

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

Syntax hints:   = wceq 1559  dom cdm 5645   Fn wfn 6512

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 209  df-an 400  df-fn 6520

This theorem is referenced by:  dmmpti  6661  dmmpo  8048  tfr2  8364  tz7.44-2  8373  rdgsuc  8390  tz7.48-2  8408  tz7.48-1  8409  tz7.48-3  8410  tz7.49  8411  brwitnlem  8471  om0x  8483  naddcllem  8641  naddov2  8644  naddasslem1  8660  naddasslem2  8661  elpmi  8823  elmapex  8825  pmresg  8848  pmsspw  8855  r1suc  9725  r1ord  9735  r1ord3  9737  onwf  9785  r1val3  9793  r1pw  9800  rankr1b  9819  alephcard  10023  alephnbtwn  10024  alephgeom  10035  dfac12lem2  10098  alephsing  10230  hsmexlem6  10385  zorn2lem4  10453  alephadd  10532  alephreg  10537  pwcfsdom  10538  r1limwun  10691  r1wunlim  10692  rankcf  10732  inatsk  10733  r1tskina  10737  dmaddpi  10845  dmmulpi  10846  seqexw  14027  hashkf  14342  bpolylem  16061  0rest  17441  firest  17444  homfeqbas  17711  cidpropd  17725  2oppchomf  17739  fucbas  17979  fuchom  17980  xpccofval  18197  oppchofcl  18275  oyoncl  18285  ex-chn2  18653  mulgfval  19094  gicer  19300  psgneldm  19526  psgneldm2  19527  psgnval  19530  psgnghm  21612  psgnghm2  21613  cldrcl  23066  iscldtop  23135  restrcl  23197  ssrest  23216  resstopn  23226  hmpher  23824  nghmfval  24762  isnghm  24763  bdaydm  27819  newval  27905  negsproplem2  28099  r1wf  35356  r1elcl  35358  cvmtop1  35574  cvmtop2  35575  imageval  36242  filnetlem4  36705  ismrc  43246  dnnumch3lem  43587  dnnumch3  43588  aomclem4  43598  grur1cld  44772  gricrel  48505  grlicrel  48592  fonex  49452  cicrcl2  49628  cic1st2nd  49632  oppfrcl  49713  eloppf  49718  initopropdlemlem  49824  initopropd  49828  termopropd  49829  zeroopropd  49830  reldmxpc  49831  reldmlan2  50202  reldmran2  50203  lanrcl  50206  ranrcl  50207