Theorem fndm 5354

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4660  Fun wfun 5249   Fn wfn 5250

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 5258

This theorem is referenced by:  funfni  5355  fndmu  5356  fnbr  5357  fnco  5363  fnresdm  5364  fnresdisj  5365  fnssresb  5367  fn0  5374  fnimadisj  5375  fnimaeq0  5376  dmmpti  5384  fdm  5410  f1dm  5465  f1odm  5505  f1o00  5536  fvelimab  5614  fvun1  5624  eqfnfv2  5657  fndmdif  5664  fneqeql2  5668  elpreima  5678  fsn2  5733  fconst3m  5778  fconst4m  5779  fnfvima  5794  funiunfvdm  5807  fnunirn  5811  dff13  5812  f1eqcocnv  5835  oprssov  6062  offval  6140  ofrfval  6141  fnexALT  6165  dmmpo  6259  dmmpoga  6263  tposfo2  6322  smodm2  6350  smoel2  6358  tfrlem5  6369  tfrlem8  6373  tfrlem9  6374  tfrlemisucaccv  6380  tfrlemiubacc  6385  tfrexlem  6389  tfri2d  6391  tfr1onlemsucaccv  6396  tfr1onlemubacc  6401  tfrcllemsucaccv  6409  tfri2  6421  rdgivallem  6436  ixpprc  6775  ixpssmap2g  6783  ixpssmapg  6784  bren  6803  fndmeng  6866  caseinl  7152  caseinr  7153  cc2lem  7328  dmaddpi  7387  dmmulpi  7388  hashinfom  10852  shftfn  10971  phimullem  12366  ennnfonelemhom  12575  qnnen  12591  fnpr2ob  12926  cldrcl  14281  neiss2  14321  txdis1cn  14457