Theorem fndm 5426

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4723  Fun wfun 5318   Fn wfn 5319

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 5327

This theorem is referenced by:  fndmi  5427  fndmd  5428  funfni  5429  fndmu  5430  fnbr  5431  fnco  5437  fnresdm  5438  fnresdisj  5439  fnssresb  5441  fn0  5449  fnimadisj  5450  fnimaeq0  5451  dmmpti  5459  fdm  5485  f1dm  5544  f1odm  5584  f1o00  5616  fvelimab  5698  fvun1  5708  eqfnfv2  5741  fndmdif  5748  fneqeql2  5752  elpreima  5762  fsn2  5817  fncofn  5827  fconst3m  5868  fconst4m  5869  fnfvima  5884  funiunfvdm  5899  fnunirn  5903  dff13  5904  f1eqcocnv  5927  oprssov  6159  offval  6238  ofrfval  6239  fnexALT  6268  dmmpo  6364  dmmpoga  6368  tposfo2  6428  smodm2  6456  smoel2  6464  tfrlem5  6475  tfrlem8  6479  tfrlem9  6480  tfrlemisucaccv  6486  tfrlemiubacc  6491  tfrexlem  6495  tfri2d  6497  tfr1onlemsucaccv  6502  tfr1onlemubacc  6507  tfrcllemsucaccv  6515  tfri2  6527  rdgivallem  6542  ixpprc  6883  ixpssmap2g  6891  ixpssmapg  6892  bren  6912  fndmeng  6980  caseinl  7281  caseinr  7282  cc2lem  7475  dmaddpi  7535  dmmulpi  7536  hashinfom  11030  shftfn  11375  phimullem  12787  ennnfonelemhom  13026  qnnen  13042  fnpr2ob  13413  cldrcl  14816  neiss2  14856  txdis1cn  14992  uhgrm  15919  upgrfnen  15939  upgrex  15944  umgrfnen  15949