Theorem fndmi 6430

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

Syntax hints:   = wceq 1539  dom cdm 5517   Fn wfn 6323

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 401  df-fn 6331

This theorem is referenced by:  dmmpti  6468  dmmpo  7766  tfr2  8037  tz7.44-2  8046  rdgsuc  8063  tz7.48-2  8081  tz7.48-1  8082  tz7.48-3  8083  tz7.49  8084  brwitnlem  8135  om0x  8147  elpmi  8428  elmapex  8430  pmresg  8445  pmsspw  8452  r1suc  9217  r1ord  9227  r1ord3  9229  onwf  9277  r1val3  9285  r1pw  9292  rankr1b  9311  alephcard  9515  alephnbtwn  9516  alephgeom  9527  dfac12lem2  9589  alephsing  9721  hsmexlem6  9876  zorn2lem4  9944  alephadd  10022  alephreg  10027  pwcfsdom  10028  r1limwun  10181  r1wunlim  10182  rankcf  10222  inatsk  10223  r1tskina  10227  dmaddpi  10335  dmmulpi  10336  seqexw  13419  hashkf  13727  bpolylem  15435  0rest  16746  firest  16749  homfeqbas  17009  cidpropd  17023  2oppchomf  17037  fucbas  17274  fuchom  17275  xpccofval  17483  oppchofcl  17561  oyoncl  17571  mulgfval  18278  gicer  18468  psgneldm  18683  psgneldm2  18684  psgnval  18687  psgnghm  20330  psgnghm2  20331  cldrcl  21711  iscldtop  21780  restrcl  21842  ssrest  21861  resstopn  21871  hmpher  22469  nghmfval  23409  isnghm  23410  cvmtop1  32723  cvmtop2  32724  imageval  33766  filnetlem4  34104  ismrc  40000  dnnumch3lem  40348  dnnumch3  40349  aomclem4  40359  grur1cld  41298