Theorem fndm 5287

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

Syntax hints:   → wi 4   = wceq 1343  dom cdm 4604  Fun wfun 5182   Fn wfn 5183

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

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

This theorem is referenced by:  funfni  5288  fndmu  5289  fnbr  5290  fnco  5296  fnresdm  5297  fnresdisj  5298  fnssresb  5300  fn0  5307  fnimadisj  5308  fnimaeq0  5309  dmmpti  5317  fdm  5343  f1dm  5398  f1odm  5436  f1o00  5467  fvelimab  5542  fvun1  5552  eqfnfv2  5584  fndmdif  5590  fneqeql2  5594  elpreima  5604  fsn2  5659  fconst3m  5704  fconst4m  5705  fnfvima  5719  funiunfvdm  5731  fnunirn  5735  dff13  5736  f1eqcocnv  5759  oprssov  5983  offval  6057  ofrfval  6058  fnexALT  6079  dmmpo  6173  dmmpoga  6176  tposfo2  6235  smodm2  6263  smoel2  6271  tfrlem5  6282  tfrlem8  6286  tfrlem9  6287  tfrlemisucaccv  6293  tfrlemiubacc  6298  tfrexlem  6302  tfri2d  6304  tfr1onlemsucaccv  6309  tfr1onlemubacc  6314  tfrcllemsucaccv  6322  tfri2  6334  rdgivallem  6349  ixpprc  6685  ixpssmap2g  6693  ixpssmapg  6694  bren  6713  fndmeng  6776  caseinl  7056  caseinr  7057  cc2lem  7207  dmaddpi  7266  dmmulpi  7267  hashinfom  10691  shftfn  10766  phimullem  12157  ennnfonelemhom  12348  qnnen  12364  cldrcl  12742  neiss2  12782  txdis1cn  12918