Theorem fndm 5353

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

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

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 5257

This theorem is referenced by:  funfni  5354  fndmu  5355  fnbr  5356  fnco  5362  fnresdm  5363  fnresdisj  5364  fnssresb  5366  fn0  5373  fnimadisj  5374  fnimaeq0  5375  dmmpti  5383  fdm  5409  f1dm  5464  f1odm  5504  f1o00  5535  fvelimab  5613  fvun1  5623  eqfnfv2  5656  fndmdif  5663  fneqeql2  5667  elpreima  5677  fsn2  5732  fconst3m  5777  fconst4m  5778  fnfvima  5793  funiunfvdm  5806  fnunirn  5810  dff13  5811  f1eqcocnv  5834  oprssov  6060  offval  6138  ofrfval  6139  fnexALT  6163  dmmpo  6258  dmmpoga  6261  tposfo2  6320  smodm2  6348  smoel2  6356  tfrlem5  6367  tfrlem8  6371  tfrlem9  6372  tfrlemisucaccv  6378  tfrlemiubacc  6383  tfrexlem  6387  tfri2d  6389  tfr1onlemsucaccv  6394  tfr1onlemubacc  6399  tfrcllemsucaccv  6407  tfri2  6419  rdgivallem  6434  ixpprc  6773  ixpssmap2g  6781  ixpssmapg  6782  bren  6801  fndmeng  6864  caseinl  7150  caseinr  7151  cc2lem  7326  dmaddpi  7385  dmmulpi  7386  hashinfom  10849  shftfn  10968  phimullem  12363  ennnfonelemhom  12572  qnnen  12588  fnpr2ob  12923  cldrcl  14270  neiss2  14310  txdis1cn  14446