Theorem fndm 5420

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 5321	. 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 1395   dom cdm 4719   Fun wfun 5312   Fn wfn 5313

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 5321

This theorem is referenced by:  fndmi  5421  fndmd  5422  funfni  5423  fndmu  5424  fnbr  5425  fnco  5431  fnresdm  5432  fnresdisj  5433  fnssresb  5435  fn0  5443  fnimadisj  5444  fnimaeq0  5445  dmmpti  5453  fdm  5479  f1dm  5536  f1odm  5576  f1o00  5608  fvelimab  5690  fvun1  5700  eqfnfv2  5733  fndmdif  5740  fneqeql2  5744  elpreima  5754  fsn2  5809  fconst3m  5858  fconst4m  5859  fnfvima  5874  funiunfvdm  5887  fnunirn  5891  dff13  5892  f1eqcocnv  5915  oprssov  6147  offval  6226  ofrfval  6227  fnexALT  6256  dmmpo  6350  dmmpoga  6354  tposfo2  6413  smodm2  6441  smoel2  6449  tfrlem5  6460  tfrlem8  6464  tfrlem9  6465  tfrlemisucaccv  6471  tfrlemiubacc  6476  tfrexlem  6480  tfri2d  6482  tfr1onlemsucaccv  6487  tfr1onlemubacc  6492  tfrcllemsucaccv  6500  tfri2  6512  rdgivallem  6527  ixpprc  6866  ixpssmap2g  6874  ixpssmapg  6875  bren  6895  fndmeng  6963  caseinl  7258  caseinr  7259  cc2lem  7452  dmaddpi  7512  dmmulpi  7513  hashinfom  11000  shftfn  11335  phimullem  12747  ennnfonelemhom  12986  qnnen  13002  fnpr2ob  13373  cldrcl  14776  neiss2  14816  txdis1cn  14952  uhgrm  15878  upgrfnen  15898  upgrex  15903  umgrfnen  15908