Theorem fndm 4941

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

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

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 4848

This theorem is referenced by:  funfni  4942  fndmu  4943  fnbr  4944  fnco  4950  fnresdm  4951  fnresdisj  4952  fnssresb  4954  fn0  4961  fnimadisj  4962  fnimaeq0  4963  dmmpti  4971  fdm  4993  f1dm  5039  f1odm  5073  f1o00  5104  fvelimab  5172  fvun1  5182  eqfnfv2  5209  fndmdif  5215  fneqeql2  5219  elpreima  5229  fsn2  5280  fconst3m  5323  fconst4m  5324  fnfvima  5336  funiunfvdm  5345  fnunirn  5349  dff13  5350  f1eqcocnv  5374  oprssov  5584  offval  5661  ofrfval  5662  fnexALT  5682  dmmpt2  5773  tposfo2  5823  smodm2  5851  smoel2  5859  tfrlem5  5871  tfrlem8  5875  tfrlem9  5876  tfrlemisucaccv  5880  tfrlemiubacc  5885  tfrexlem  5889  tfri2d  5891  tfri2  5893  rdgivallem  5908  frecsuclemdm  5927  bren  6164  fndmeng  6225  dmaddpi  6309  dmmulpi  6310