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  6542  smodm2  6570  smoel2  6578  tfrlem5  6589  tfrlem8  6593  tfrlem9  6594  tfrlemisucaccv  6600  tfrlemiubacc  6605  tfrexlem  6609  tfri2d  6611  tfr1onlemsucaccv  6616  tfr1onlemubacc  6621  tfrcllemsucaccv  6629  tfri2  6641  rdgivallem  6656  ixpprc  7005  ixpssmap2g  7013  ixpssmapg  7014  bren  7034  fndmeng  7102  caseinl  7437  caseinr  7438  cc2lem  7638  dmaddpi  7698  dmmulpi  7699  hashinfom  11239  shftfn  11611  phimullem  13032  ennnfonelemhom  13364  qnnen  13380  fnpr2ob  13720  cldrcl  15328  neiss2  15368  txdis1cn  15504  uhgrm  16524  upgrfnen  16544  upgrex  16549  umgrfnen  16554