Theorem fndm 5029

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 4935	. 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 1285   dom cdm 4371   Fun wfun 4926   Fn wfn 4927

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 4935

This theorem is referenced by:  funfni  5030  fndmu  5031  fnbr  5032  fnco  5038  fnresdm  5039  fnresdisj  5040  fnssresb  5042  fn0  5049  fnimadisj  5050  fnimaeq0  5051  dmmpti  5059  fdm  5081  f1dm  5127  f1odm  5161  f1o00  5192  fvelimab  5261  fvun1  5271  eqfnfv2  5298  fndmdif  5304  fneqeql2  5308  elpreima  5318  fsn2  5369  fconst3m  5412  fconst4m  5413  fnfvima  5425  funiunfvdm  5434  fnunirn  5438  dff13  5439  f1eqcocnv  5462  oprssov  5673  offval  5750  ofrfval  5751  fnexALT  5771  dmmpt2  5862  tposfo2  5916  smodm2  5944  smoel2  5952  tfrlem5  5963  tfrlem8  5967  tfrlem9  5968  tfrlemisucaccv  5974  tfrlemiubacc  5979  tfrexlem  5983  tfri2d  5985  tfr1onlemsucaccv  5990  tfr1onlemubacc  5995  tfrcllemsucaccv  6003  tfri2  6015  rdgivallem  6030  bren  6294  fndmeng  6357  dmaddpi  6577  dmmulpi  6578  sizeinf  9802  shftfn  9850