Theorem fndm 4939

Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fndm	⊢ (𝐹 Fn A → dom 𝐹 = A)

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 4847	. 2 ⊢ (𝐹 Fn A ↔ (Fun 𝐹 ∧ dom 𝐹 = A))
2	1	simprbi 260	1 ⊢ (𝐹 Fn A → dom 𝐹 = A)

Syntax hints:   → wi 4   = wceq 1242  dom cdm 4287  Fun wfun 4838   Fn wfn 4839

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem depends on definitions:  df-bi 110  df-fn 4847

This theorem is referenced by:  funfni  4940  fndmu  4941  fnbr  4942  fnco  4948  fnresdm  4949  fnresdisj  4950  fnssresb  4952  fn0  4959  fnimadisj  4960  fnimaeq0  4961  dmmpti  4969  fdm  4991  f1dm  5037  f1odm  5071  f1o00  5102  fvelimab  5170  fvun1  5180  eqfnfv2  5207  fndmdif  5213  fneqeql2  5217  elpreima  5227  fsn2  5278  fconst3m  5321  fconst4m  5322  fnfvima  5334  funiunfvdm  5343  fnunirn  5347  dff13  5348  f1eqcocnv  5372  oprssov  5581  offval  5658  ofrfval  5659  fnexALT  5679  dmmpt2  5770  tposfo2  5820  smodm2  5848  smoel2  5856  tfrlem5  5868  tfrlem8  5872  tfrlem9  5873  tfrlemisucaccv  5877  tfrlemiubacc  5882  tfrexlem  5886  tfri2d  5888  tfri2  5890  rdgivallem  5905  frecsuclemdm  5921  bren  6157  fndmeng  6218  dmaddpi  6302  dmmulpi  6303