Theorem fndm 5222

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

Syntax hints:   → wi 4   = wceq 1331  dom cdm 4539  Fun wfun 5117   Fn wfn 5118

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 5126

This theorem is referenced by:  funfni  5223  fndmu  5224  fnbr  5225  fnco  5231  fnresdm  5232  fnresdisj  5233  fnssresb  5235  fn0  5242  fnimadisj  5243  fnimaeq0  5244  dmmpti  5252  fdm  5278  f1dm  5333  f1odm  5371  f1o00  5402  fvelimab  5477  fvun1  5487  eqfnfv2  5519  fndmdif  5525  fneqeql2  5529  elpreima  5539  fsn2  5594  fconst3m  5639  fconst4m  5640  fnfvima  5652  funiunfvdm  5664  fnunirn  5668  dff13  5669  f1eqcocnv  5692  oprssov  5912  offval  5989  ofrfval  5990  fnexALT  6011  dmmpo  6103  dmmpoga  6106  tposfo2  6164  smodm2  6192  smoel2  6200  tfrlem5  6211  tfrlem8  6215  tfrlem9  6216  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfrexlem  6231  tfri2d  6233  tfr1onlemsucaccv  6238  tfr1onlemubacc  6243  tfrcllemsucaccv  6251  tfri2  6263  rdgivallem  6278  ixpprc  6613  ixpssmap2g  6621  ixpssmapg  6622  bren  6641  fndmeng  6704  caseinl  6976  caseinr  6977  dmaddpi  7133  dmmulpi  7134  hashinfom  10524  shftfn  10596  phimullem  11901  ennnfonelemhom  11928  qnnen  11944  cldrcl  12271  neiss2  12311  txdis1cn  12447