Theorem fndm 5455

Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fndm	⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 5355	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 275	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4749  Fun wfun 5346   Fn wfn 5347

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 5355

This theorem is referenced by:  fndmi  5456  fndmd  5457  funfni  5458  fndmu  5459  fnbr  5460  fnco  5466  fnresdm  5467  fnresdisj  5468  fnssresb  5470  fn0  5478  fnimadisj  5479  fnimaeq0  5480  dmmpti  5488  fdm  5514  f1dm  5578  f1odm  5618  f1o00  5651  fvelimab  5733  fvun1  5743  eqfnfv2  5776  fndmdif  5783  fneqeql2  5787  elpreima  5797  fsn2  5851  fncofn  5862  fconst3m  5903  fconst4m  5904  fnfvima  5921  funiunfvdm  5936  fnunirn  5940  dff13  5941  f1eqcocnv  5964  oprssov  6196  offval  6274  ofrfval  6275  fnexALT  6304  dmmpo  6400  dmmpoga  6404  suppvalfng  6440  suppvalfn  6441  suppfnss  6457  tposfo2  6498  smodm2  6526  smoel2  6534  tfrlem5  6545  tfrlem8  6549  tfrlem9  6550  tfrlemisucaccv  6556  tfrlemiubacc  6561  tfrexlem  6565  tfri2d  6567  tfr1onlemsucaccv  6572  tfr1onlemubacc  6577  tfrcllemsucaccv  6585  tfri2  6597  rdgivallem  6612  ixpprc  6954  ixpssmap2g  6962  ixpssmapg  6963  bren  6983  fndmeng  7051  caseinl  7382  caseinr  7383  cc2lem  7580  dmaddpi  7640  dmmulpi  7641  hashinfom  11141  shftfn  11509  phimullem  12922  ennnfonelemhom  13166  qnnen  13182  fnpr2ob  13553  cldrcl  14967  neiss2  15007  txdis1cn  15143  uhgrm  16073  upgrfnen  16093  upgrex  16098  umgrfnen  16103