Theorem fndm 5358

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4664  Fun wfun 5253   Fn wfn 5254

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 5262

This theorem is referenced by:  funfni  5359  fndmu  5360  fnbr  5361  fnco  5367  fnresdm  5368  fnresdisj  5369  fnssresb  5371  fn0  5378  fnimadisj  5379  fnimaeq0  5380  dmmpti  5388  fdm  5414  f1dm  5469  f1odm  5509  f1o00  5540  fvelimab  5618  fvun1  5628  eqfnfv2  5661  fndmdif  5668  fneqeql2  5672  elpreima  5682  fsn2  5737  fconst3m  5782  fconst4m  5783  fnfvima  5798  funiunfvdm  5811  fnunirn  5815  dff13  5816  f1eqcocnv  5839  oprssov  6066  offval  6144  ofrfval  6145  fnexALT  6169  dmmpo  6263  dmmpoga  6267  tposfo2  6326  smodm2  6354  smoel2  6362  tfrlem5  6373  tfrlem8  6377  tfrlem9  6378  tfrlemisucaccv  6384  tfrlemiubacc  6389  tfrexlem  6393  tfri2d  6395  tfr1onlemsucaccv  6400  tfr1onlemubacc  6405  tfrcllemsucaccv  6413  tfri2  6425  rdgivallem  6440  ixpprc  6779  ixpssmap2g  6787  ixpssmapg  6788  bren  6807  fndmeng  6870  caseinl  7158  caseinr  7159  cc2lem  7335  dmaddpi  7394  dmmulpi  7395  hashinfom  10872  shftfn  10991  phimullem  12403  ennnfonelemhom  12642  qnnen  12658  fnpr2ob  12993  cldrcl  14348  neiss2  14388  txdis1cn  14524