Theorem fndmi 6651

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

Syntax hints:   = wceq 1542  dom cdm 5676   Fn wfn 6536

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 6544

This theorem is referenced by:  dmmpti  6692  dmmpo  8054  tfr2  8395  tz7.44-2  8404  rdgsuc  8421  tz7.48-2  8439  tz7.48-1  8440  tz7.48-3  8441  tz7.49  8442  brwitnlem  8504  om0x  8516  naddcllem  8672  naddov2  8675  naddasslem1  8690  naddasslem2  8691  elpmi  8837  elmapex  8839  pmresg  8861  pmsspw  8868  r1suc  9762  r1ord  9772  r1ord3  9774  onwf  9822  r1val3  9830  r1pw  9837  rankr1b  9856  alephcard  10062  alephnbtwn  10063  alephgeom  10074  dfac12lem2  10136  alephsing  10268  hsmexlem6  10423  zorn2lem4  10491  alephadd  10569  alephreg  10574  pwcfsdom  10575  r1limwun  10728  r1wunlim  10729  rankcf  10769  inatsk  10770  r1tskina  10774  dmaddpi  10882  dmmulpi  10883  seqexw  13979  hashkf  14289  bpolylem  15989  0rest  17372  firest  17375  homfeqbas  17637  cidpropd  17651  2oppchomf  17667  fucbas  17909  fuchom  17910  fuchomOLD  17911  xpccofval  18131  oppchofcl  18210  oyoncl  18220  mulgfval  18947  gicer  19145  psgneldm  19366  psgneldm2  19367  psgnval  19370  psgnghm  21125  psgnghm2  21126  cldrcl  22522  iscldtop  22591  restrcl  22653  ssrest  22672  resstopn  22682  hmpher  23280  nghmfval  24231  isnghm  24232  newval  27340  negsproplem2  27493  cvmtop1  34240  cvmtop2  34241  imageval  34891  filnetlem4  35255  ismrc  41425  dnnumch3lem  41774  dnnumch3  41775  aomclem4  41785  grur1cld  42977