Theorem fndmi 6460

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

Syntax hints:   = wceq 1543  dom cdm 5536   Fn wfn 6353

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 210  df-an 400  df-fn 6361

This theorem is referenced by:  dmmpti  6500  dmmpo  7819  tfr2  8112  tz7.44-2  8121  rdgsuc  8138  tz7.48-2  8156  tz7.48-1  8157  tz7.48-3  8158  tz7.49  8159  brwitnlem  8212  om0x  8224  elpmi  8505  elmapex  8507  pmresg  8529  pmsspw  8536  r1suc  9351  r1ord  9361  r1ord3  9363  onwf  9411  r1val3  9419  r1pw  9426  rankr1b  9445  alephcard  9649  alephnbtwn  9650  alephgeom  9661  dfac12lem2  9723  alephsing  9855  hsmexlem6  10010  zorn2lem4  10078  alephadd  10156  alephreg  10161  pwcfsdom  10162  r1limwun  10315  r1wunlim  10316  rankcf  10356  inatsk  10357  r1tskina  10361  dmaddpi  10469  dmmulpi  10470  seqexw  13555  hashkf  13863  bpolylem  15573  0rest  16888  firest  16891  homfeqbas  17153  cidpropd  17167  2oppchomf  17182  fucbas  17422  fuchom  17423  fuchomOLD  17424  xpccofval  17643  oppchofcl  17722  oyoncl  17732  mulgfval  18444  gicer  18634  psgneldm  18849  psgneldm2  18850  psgnval  18853  psgnghm  20496  psgnghm2  20497  cldrcl  21877  iscldtop  21946  restrcl  22008  ssrest  22027  resstopn  22037  hmpher  22635  nghmfval  23574  isnghm  23575  cvmtop1  32889  cvmtop2  32890  naddcllem  33517  naddov2  33520  newval  33725  imageval  33918  filnetlem4  34256  ismrc  40167  dnnumch3lem  40515  dnnumch3  40516  aomclem4  40526  grur1cld  41464