Theorem fndmi 6539

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

Syntax hints:   = wceq 1539  dom cdm 5591   Fn wfn 6430

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 397  df-fn 6438

This theorem is referenced by:  dmmpti  6579  dmmpo  7911  tfr2  8227  tz7.44-2  8236  rdgsuc  8253  tz7.48-2  8271  tz7.48-1  8272  tz7.48-3  8273  tz7.49  8274  brwitnlem  8335  om0x  8347  elpmi  8632  elmapex  8634  pmresg  8656  pmsspw  8663  r1suc  9526  r1ord  9536  r1ord3  9538  onwf  9586  r1val3  9594  r1pw  9601  rankr1b  9620  alephcard  9824  alephnbtwn  9825  alephgeom  9836  dfac12lem2  9898  alephsing  10030  hsmexlem6  10185  zorn2lem4  10253  alephadd  10331  alephreg  10336  pwcfsdom  10337  r1limwun  10490  r1wunlim  10491  rankcf  10531  inatsk  10532  r1tskina  10536  dmaddpi  10644  dmmulpi  10645  seqexw  13735  hashkf  14044  bpolylem  15756  0rest  17138  firest  17141  homfeqbas  17403  cidpropd  17417  2oppchomf  17433  fucbas  17675  fuchom  17676  fuchomOLD  17677  xpccofval  17897  oppchofcl  17976  oyoncl  17986  mulgfval  18700  gicer  18890  psgneldm  19109  psgneldm2  19110  psgnval  19113  psgnghm  20783  psgnghm2  20784  cldrcl  22175  iscldtop  22244  restrcl  22306  ssrest  22325  resstopn  22335  hmpher  22933  nghmfval  23884  isnghm  23885  cvmtop1  33219  cvmtop2  33220  naddcllem  33828  naddov2  33831  newval  34036  imageval  34229  filnetlem4  34567  ismrc  40520  dnnumch3lem  40868  dnnumch3  40869  aomclem4  40879  grur1cld  41820