Theorem fndm 5374

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 5275	. 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 1373   dom cdm 4676   Fun wfun 5266   Fn wfn 5267

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 5275

This theorem is referenced by:  fndmi  5375  fndmd  5376  funfni  5377  fndmu  5378  fnbr  5379  fnco  5385  fnresdm  5386  fnresdisj  5387  fnssresb  5389  fn0  5397  fnimadisj  5398  fnimaeq0  5399  dmmpti  5407  fdm  5433  f1dm  5488  f1odm  5528  f1o00  5559  fvelimab  5637  fvun1  5647  eqfnfv2  5680  fndmdif  5687  fneqeql2  5691  elpreima  5701  fsn2  5756  fconst3m  5805  fconst4m  5806  fnfvima  5821  funiunfvdm  5834  fnunirn  5838  dff13  5839  f1eqcocnv  5862  oprssov  6090  offval  6168  ofrfval  6169  fnexALT  6198  dmmpo  6292  dmmpoga  6296  tposfo2  6355  smodm2  6383  smoel2  6391  tfrlem5  6402  tfrlem8  6406  tfrlem9  6407  tfrlemisucaccv  6413  tfrlemiubacc  6418  tfrexlem  6422  tfri2d  6424  tfr1onlemsucaccv  6429  tfr1onlemubacc  6434  tfrcllemsucaccv  6442  tfri2  6454  rdgivallem  6469  ixpprc  6808  ixpssmap2g  6816  ixpssmapg  6817  bren  6837  fndmeng  6904  caseinl  7195  caseinr  7196  cc2lem  7380  dmaddpi  7440  dmmulpi  7441  hashinfom  10925  shftfn  11168  phimullem  12580  ennnfonelemhom  12819  qnnen  12835  fnpr2ob  13205  cldrcl  14607  neiss2  14647  txdis1cn  14783