Theorem fndm 5483

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 5383	. 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 4776   Fun wfun 5374   Fn wfn 5375

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 5383

This theorem is used by:  fndmi  5484  fndmd  5485  funfni  5486  fndmu  5487  fnbr  5488  fnco  5494  fnresdm  5495  fnresdisj  5496  fnssresb  5498  fn0  5506  fnimadisj  5507  fnimaeq0  5508  dmmpti  5516  fdm  5542  f1dm  5606  f1odm  5646  f1o00  5679  fvelimab  5762  fvun1  5772  eqfnfv2  5810  fndmdif  5817  fneqeql2  5821  elpreima  5831  fsn2  5885  fncofn  5896  fconst3m  5937  fconst4m  5938  fnfvima  5956  funiunfvdm  5972  fnunirn  5976  dff13  5977  f1eqcocnv  6000  oprssov  6234  offval  6314  ofrfval  6315  fnexALT  6344  dmmpo  6444  dmmpoga  6448  suppvalfng  6484  suppvalfn  6485  suppfnss  6501  tposfo2  6543  smodm2  6571  smoel2  6579  tfrlem5  6590  tfrlem8  6594  tfrlem9  6595  tfrlemisucaccv  6601  tfrlemiubacc  6606  tfrexlem  6610  tfri2d  6612  tfr1onlemsucaccv  6617  tfr1onlemubacc  6622  tfrcllemsucaccv  6630  tfri2  6642  rdgivallem  6657  ixpprc  7007  ixpssmap2g  7015  ixpssmapg  7016  bren  7036  fndmeng  7104  caseinl  7437  caseinr  7438  cc2lem  7638  dmaddpi  7698  dmmulpi  7699  hashinfom  11238  shftfn  11610  phimullem  13031  ennnfonelemhom  13363  qnnen  13379  fnpr2ob  13719  cldrcl  15345  neiss2  15385  txdis1cn  15521  uhgrm  16541  upgrfnen  16561  upgrex  16566  umgrfnen  16571