Theorem fndmi 6654

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

Syntax hints:   = wceq 1542  dom cdm 5677   Fn wfn 6539

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 398  df-fn 6547

This theorem is referenced by:  dmmpti  6695  dmmpo  8057  tfr2  8398  tz7.44-2  8407  rdgsuc  8424  tz7.48-2  8442  tz7.48-1  8443  tz7.48-3  8444  tz7.49  8445  brwitnlem  8507  om0x  8519  naddcllem  8675  naddov2  8678  naddasslem1  8693  naddasslem2  8694  elpmi  8840  elmapex  8842  pmresg  8864  pmsspw  8871  r1suc  9765  r1ord  9775  r1ord3  9777  onwf  9825  r1val3  9833  r1pw  9840  rankr1b  9859  alephcard  10065  alephnbtwn  10066  alephgeom  10077  dfac12lem2  10139  alephsing  10271  hsmexlem6  10426  zorn2lem4  10494  alephadd  10572  alephreg  10577  pwcfsdom  10578  r1limwun  10731  r1wunlim  10732  rankcf  10772  inatsk  10773  r1tskina  10777  dmaddpi  10885  dmmulpi  10886  seqexw  13982  hashkf  14292  bpolylem  15992  0rest  17375  firest  17378  homfeqbas  17640  cidpropd  17654  2oppchomf  17670  fucbas  17912  fuchom  17913  fuchomOLD  17914  xpccofval  18134  oppchofcl  18213  oyoncl  18223  mulgfval  18952  gicer  19150  psgneldm  19371  psgneldm2  19372  psgnval  19375  psgnghm  21133  psgnghm2  21134  cldrcl  22530  iscldtop  22599  restrcl  22661  ssrest  22680  resstopn  22690  hmpher  23288  nghmfval  24239  isnghm  24240  newval  27350  negsproplem2  27503  cvmtop1  34251  cvmtop2  34252  imageval  34902  filnetlem4  35266  ismrc  41439  dnnumch3lem  41788  dnnumch3  41789  aomclem4  41799  grur1cld  42991