Theorem fndm 4924

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 4832	. 2 ⊢ (𝐹 Fn A ↔ (Fun 𝐹 ∧ dom 𝐹 = A))
2	1	simprbi 260	1 ⊢ (𝐹 Fn A → dom 𝐹 = A)

Syntax hints:   → wi 4   = wceq 1228  dom cdm 4272  Fun wfun 4823   Fn wfn 4824

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 4832

This theorem is referenced by:  funfni  4925  fndmu  4926  fnbr  4927  fnco  4933  fnresdm  4934  fnresdisj  4935  fnssresb  4937  fn0  4944  fnimadisj  4945  fnimaeq0  4946  dmmpti  4954  fdm  4976  f1dm  5021  f1odm  5055  f1o00  5086  fvelimab  5154  fvun1  5164  eqfnfv2  5191  fndmdif  5197  fneqeql2  5201  elpreima  5211  fsn2  5262  fconst3m  5305  fconst4m  5306  fnfvima  5318  funiunfvdm  5327  fnunirn  5331  dff13  5332  f1eqcocnv  5356  oprssov  5565  offval  5642  ofrfval  5643  fnexALT  5663  dmmpt2  5754  tposfo2  5804  smodm2  5832  smoel2  5840  tfrlem5  5852  tfrlem8  5856  tfrlem9  5857  tfrlemisucaccv  5860  tfrlemiubacc  5865  tfrexlem  5870  tfri2d  5872  tfri2  5874  rdgivallem  5888  frecsuclemdm  5904  dmaddpi  6185  dmmulpi  6186