Theorem fndm 5457

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 5357	. 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 4751   Fun wfun 5348   Fn wfn 5349

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 5357

This theorem is referenced by:  fndmi  5458  fndmd  5459  funfni  5460  fndmu  5461  fnbr  5462  fnco  5468  fnresdm  5469  fnresdisj  5470  fnssresb  5472  fn0  5480  fnimadisj  5481  fnimaeq0  5482  dmmpti  5490  fdm  5516  f1dm  5580  f1odm  5620  f1o00  5653  fvelimab  5735  fvun1  5745  eqfnfv2  5778  fndmdif  5785  fneqeql2  5789  elpreima  5799  fsn2  5853  fncofn  5864  fconst3m  5905  fconst4m  5906  fnfvima  5923  funiunfvdm  5938  fnunirn  5942  dff13  5943  f1eqcocnv  5966  oprssov  6198  offval  6276  ofrfval  6277  fnexALT  6306  dmmpo  6402  dmmpoga  6406  suppvalfng  6442  suppvalfn  6443  suppfnss  6459  tposfo2  6500  smodm2  6528  smoel2  6536  tfrlem5  6547  tfrlem8  6551  tfrlem9  6552  tfrlemisucaccv  6558  tfrlemiubacc  6563  tfrexlem  6567  tfri2d  6569  tfr1onlemsucaccv  6574  tfr1onlemubacc  6579  tfrcllemsucaccv  6587  tfri2  6599  rdgivallem  6614  ixpprc  6956  ixpssmap2g  6964  ixpssmapg  6965  bren  6985  fndmeng  7053  caseinl  7384  caseinr  7385  cc2lem  7582  dmaddpi  7642  dmmulpi  7643  hashinfom  11145  shftfn  11513  phimullem  12926  ennnfonelemhom  13183  qnnen  13199  fnpr2ob  13570  cldrcl  14984  neiss2  15024  txdis1cn  15160  uhgrm  16090  upgrfnen  16110  upgrex  16115  umgrfnen  16120