Theorem fndmi 6546

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

Syntax hints:   = wceq 1539  dom cdm 5590   Fn wfn 6432

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 6440

This theorem is referenced by:  dmmpti  6586  dmmpo  7920  tfr2  8238  tz7.44-2  8247  rdgsuc  8264  tz7.48-2  8282  tz7.48-1  8283  tz7.48-3  8284  tz7.49  8285  brwitnlem  8346  om0x  8358  elpmi  8643  elmapex  8645  pmresg  8667  pmsspw  8674  r1suc  9537  r1ord  9547  r1ord3  9549  onwf  9597  r1val3  9605  r1pw  9612  rankr1b  9631  alephcard  9835  alephnbtwn  9836  alephgeom  9847  dfac12lem2  9909  alephsing  10041  hsmexlem6  10196  zorn2lem4  10264  alephadd  10342  alephreg  10347  pwcfsdom  10348  r1limwun  10501  r1wunlim  10502  rankcf  10542  inatsk  10543  r1tskina  10547  dmaddpi  10655  dmmulpi  10656  seqexw  13746  hashkf  14055  bpolylem  15767  0rest  17149  firest  17152  homfeqbas  17414  cidpropd  17428  2oppchomf  17444  fucbas  17686  fuchom  17687  fuchomOLD  17688  xpccofval  17908  oppchofcl  17987  oyoncl  17997  mulgfval  18711  gicer  18901  psgneldm  19120  psgneldm2  19121  psgnval  19124  psgnghm  20794  psgnghm2  20795  cldrcl  22186  iscldtop  22255  restrcl  22317  ssrest  22336  resstopn  22346  hmpher  22944  nghmfval  23895  isnghm  23896  cvmtop1  33231  cvmtop2  33232  naddcllem  33840  naddov2  33843  newval  34048  imageval  34241  filnetlem4  34579  ismrc  40530  dnnumch3lem  40878  dnnumch3  40879  aomclem4  40889  grur1cld  41857