Theorem fndm 5018

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

Assertion

Ref	Expression
fndm	|- ( F Fn A -> dom F = A )

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 4925	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simprbi 269	1 |- ( F Fn A -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1284   dom cdm 4363   Fun wfun 4916   Fn wfn 4917

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

This theorem depends on definitions:  df-bi 115  df-fn 4925

This theorem is referenced by:  funfni  5019  fndmu  5020  fnbr  5021  fnco  5027  fnresdm  5028  fnresdisj  5029  fnssresb  5031  fn0  5038  fnimadisj  5039  fnimaeq0  5040  dmmpti  5048  fdm  5070  f1dm  5116  f1odm  5150  f1o00  5181  fvelimab  5250  fvun1  5260  eqfnfv2  5287  fndmdif  5293  fneqeql2  5297  elpreima  5307  fsn2  5358  fconst3m  5401  fconst4m  5402  fnfvima  5414  funiunfvdm  5423  fnunirn  5427  dff13  5428  f1eqcocnv  5451  oprssov  5662  offval  5739  ofrfval  5740  fnexALT  5760  dmmpt2  5851  tposfo2  5905  smodm2  5933  smoel2  5941  tfrlem5  5953  tfrlem8  5957  tfrlem9  5958  tfrlemisucaccv  5962  tfrlemiubacc  5967  tfrexlem  5971  tfri2d  5973  tfri2  5975  rdgivallem  5991  frecsuclemdm  6011  bren  6251  fndmeng  6312  dmaddpi  6515  dmmulpi  6516  shftfn  9712