Theorem fndm 5128

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

Syntax hints:   → wi 4   = wceq 1290  dom cdm 4454  Fun wfun 5024   Fn wfn 5025

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-fn 5033

This theorem is referenced by:  funfni  5129  fndmu  5130  fnbr  5131  fnco  5137  fnresdm  5138  fnresdisj  5139  fnssresb  5141  fn0  5148  fnimadisj  5149  fnimaeq0  5150  dmmpti  5158  fdm  5181  f1dm  5236  f1odm  5272  f1o00  5303  fvelimab  5375  fvun1  5385  eqfnfv2  5414  fndmdif  5420  fneqeql2  5424  elpreima  5434  fsn2  5487  fconst3m  5532  fconst4m  5533  fnfvima  5545  funiunfvdm  5558  fnunirn  5562  dff13  5563  f1eqcocnv  5586  oprssov  5802  offval  5879  ofrfval  5880  fnexALT  5900  dmmpt2  5991  tposfo2  6048  smodm2  6076  smoel2  6084  tfrlem5  6095  tfrlem8  6099  tfrlem9  6100  tfrlemisucaccv  6106  tfrlemiubacc  6111  tfrexlem  6115  tfri2d  6117  tfr1onlemsucaccv  6122  tfr1onlemubacc  6127  tfrcllemsucaccv  6135  tfri2  6147  rdgivallem  6162  ixpprc  6492  ixpssmap2g  6500  ixpssmapg  6501  bren  6520  fndmeng  6583  caseinl  6838  dmaddpi  6947  dmmulpi  6948  hashinfom  10249  shftfn  10321  phimullem  11542  cldrcl  11865  neiss2  11905