Theorem fndm 5480

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 5380	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simprbi 275	1 |- ( F Fn A -> dom F = A )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   dom cdm 4774   Fun wfun 5371   Fn wfn 5372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380

This theorem is used by:  fndmi  5481  fndmd  5482  funfni  5483  fndmu  5484  fnbr  5485  fnco  5491  fnresdm  5492  fnresdisj  5493  fnssresb  5495  fn0  5503  fnimadisj  5504  fnimaeq0  5505  dmmpti  5513  fdm  5539  f1dm  5603  f1odm  5643  f1o00  5676  fvelimab  5759  fvun1  5769  eqfnfv2  5807  fndmdif  5814  fneqeql2  5818  elpreima  5828  fsn2  5882  fncofn  5893  fconst3m  5934  fconst4m  5935  fnfvima  5953  funiunfvdm  5969  fnunirn  5973  dff13  5974  f1eqcocnv  5997  oprssov  6231  offval  6310  ofrfval  6311  fnexALT  6340  dmmpo  6440  dmmpoga  6444  suppvalfng  6480  suppvalfn  6481  suppfnss  6497  tposfo2  6538  smodm2  6566  smoel2  6574  tfrlem5  6585  tfrlem8  6589  tfrlem9  6590  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfrexlem  6605  tfri2d  6607  tfr1onlemsucaccv  6612  tfr1onlemubacc  6617  tfrcllemsucaccv  6625  tfri2  6637  rdgivallem  6652  ixpprc  7001  ixpssmap2g  7009  ixpssmapg  7010  bren  7030  fndmeng  7098  caseinl  7431  caseinr  7432  cc2lem  7632  dmaddpi  7692  dmmulpi  7693  hashinfom  11217  shftfn  11589  phimullem  13003  ennnfonelemhom  13306  qnnen  13322  fnpr2ob  13661  cldrcl  15203  neiss2  15243  txdis1cn  15379  uhgrm  16319  upgrfnen  16339  upgrex  16344  umgrfnen  16349