Theorem fndm 5382

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 5283	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 275	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1373  dom cdm 4683  Fun wfun 5274   Fn wfn 5275

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 5283

This theorem is referenced by:  fndmi  5383  fndmd  5384  funfni  5385  fndmu  5386  fnbr  5387  fnco  5393  fnresdm  5394  fnresdisj  5395  fnssresb  5397  fn0  5405  fnimadisj  5406  fnimaeq0  5407  dmmpti  5415  fdm  5441  f1dm  5498  f1odm  5538  f1o00  5570  fvelimab  5648  fvun1  5658  eqfnfv2  5691  fndmdif  5698  fneqeql2  5702  elpreima  5712  fsn2  5767  fconst3m  5816  fconst4m  5817  fnfvima  5832  funiunfvdm  5845  fnunirn  5849  dff13  5850  f1eqcocnv  5873  oprssov  6101  offval  6179  ofrfval  6180  fnexALT  6209  dmmpo  6303  dmmpoga  6307  tposfo2  6366  smodm2  6394  smoel2  6402  tfrlem5  6413  tfrlem8  6417  tfrlem9  6418  tfrlemisucaccv  6424  tfrlemiubacc  6429  tfrexlem  6433  tfri2d  6435  tfr1onlemsucaccv  6440  tfr1onlemubacc  6445  tfrcllemsucaccv  6453  tfri2  6465  rdgivallem  6480  ixpprc  6819  ixpssmap2g  6827  ixpssmapg  6828  bren  6848  fndmeng  6916  caseinl  7208  caseinr  7209  cc2lem  7398  dmaddpi  7458  dmmulpi  7459  hashinfom  10945  shftfn  11210  phimullem  12622  ennnfonelemhom  12861  qnnen  12877  fnpr2ob  13247  cldrcl  14649  neiss2  14689  txdis1cn  14825  uhgrm  15749  upgrfnen  15769  upgrex  15774  umgrfnen  15779