Theorem fndm 5436

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

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4731   Fun wfun 5327   Fn wfn 5328

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

This theorem depends on definitions:  df-bi 117  df-fn 5336

This theorem is referenced by:  fndmi  5437  fndmd  5438  funfni  5439  fndmu  5440  fnbr  5441  fnco  5447  fnresdm  5448  fnresdisj  5449  fnssresb  5451  fn0  5459  fnimadisj  5460  fnimaeq0  5461  dmmpti  5469  fdm  5495  f1dm  5556  f1odm  5596  f1o00  5629  fvelimab  5711  fvun1  5721  eqfnfv2  5754  fndmdif  5761  fneqeql2  5765  elpreima  5775  fsn2  5829  fncofn  5840  fconst3m  5881  fconst4m  5882  fnfvima  5899  funiunfvdm  5914  fnunirn  5918  dff13  5919  f1eqcocnv  5942  oprssov  6174  offval  6252  ofrfval  6253  fnexALT  6282  dmmpo  6378  dmmpoga  6382  suppvalfng  6418  suppvalfn  6419  suppfnss  6435  tposfo2  6476  smodm2  6504  smoel2  6512  tfrlem5  6523  tfrlem8  6527  tfrlem9  6528  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfrexlem  6543  tfri2d  6545  tfr1onlemsucaccv  6550  tfr1onlemubacc  6555  tfrcllemsucaccv  6563  tfri2  6575  rdgivallem  6590  ixpprc  6931  ixpssmap2g  6939  ixpssmapg  6940  bren  6960  fndmeng  7028  caseinl  7350  caseinr  7351  cc2lem  7545  dmaddpi  7605  dmmulpi  7606  hashinfom  11103  shftfn  11464  phimullem  12877  ennnfonelemhom  13116  qnnen  13132  fnpr2ob  13503  cldrcl  14913  neiss2  14953  txdis1cn  15089  uhgrm  16019  upgrfnen  16039  upgrex  16044  umgrfnen  16049