Theorem fndm 4998

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

Assertion

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

Proof of Theorem fndm

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

Syntax hints:   → wi 4   = wceq 1243  dom cdm 4345  Fun wfun 4896   Fn wfn 4897

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 4905

This theorem is referenced by:  funfni  4999  fndmu  5000  fnbr  5001  fnco  5007  fnresdm  5008  fnresdisj  5009  fnssresb  5011  fn0  5018  fnimadisj  5019  fnimaeq0  5020  dmmpti  5028  fdm  5050  f1dm  5096  f1odm  5130  f1o00  5161  fvelimab  5229  fvun1  5239  eqfnfv2  5266  fndmdif  5272  fneqeql2  5276  elpreima  5286  fsn2  5337  fconst3m  5380  fconst4m  5381  fnfvima  5393  funiunfvdm  5402  fnunirn  5406  dff13  5407  f1eqcocnv  5431  oprssov  5642  offval  5719  ofrfval  5720  fnexALT  5740  dmmpt2  5831  tposfo2  5882  smodm2  5910  smoel2  5918  tfrlem5  5930  tfrlem8  5934  tfrlem9  5935  tfrlemisucaccv  5939  tfrlemiubacc  5944  tfrexlem  5948  tfri2d  5950  tfri2  5952  rdgivallem  5968  frecsuclemdm  5988  bren  6228  fndmeng  6289  dmaddpi  6423  dmmulpi  6424  shftfn  9425