Theorem fndm 5268

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

Syntax hints:   → wi 4   = wceq 1335  dom cdm 4585  Fun wfun 5163   Fn wfn 5164

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 5172

This theorem is referenced by:  funfni  5269  fndmu  5270  fnbr  5271  fnco  5277  fnresdm  5278  fnresdisj  5279  fnssresb  5281  fn0  5288  fnimadisj  5289  fnimaeq0  5290  dmmpti  5298  fdm  5324  f1dm  5379  f1odm  5417  f1o00  5448  fvelimab  5523  fvun1  5533  eqfnfv2  5565  fndmdif  5571  fneqeql2  5575  elpreima  5585  fsn2  5640  fconst3m  5685  fconst4m  5686  fnfvima  5698  funiunfvdm  5710  fnunirn  5714  dff13  5715  f1eqcocnv  5738  oprssov  5959  offval  6036  ofrfval  6037  fnexALT  6058  dmmpo  6150  dmmpoga  6153  tposfo2  6211  smodm2  6239  smoel2  6247  tfrlem5  6258  tfrlem8  6262  tfrlem9  6263  tfrlemisucaccv  6269  tfrlemiubacc  6274  tfrexlem  6278  tfri2d  6280  tfr1onlemsucaccv  6285  tfr1onlemubacc  6290  tfrcllemsucaccv  6298  tfri2  6310  rdgivallem  6325  ixpprc  6661  ixpssmap2g  6669  ixpssmapg  6670  bren  6689  fndmeng  6752  caseinl  7029  caseinr  7030  cc2lem  7180  dmaddpi  7239  dmmulpi  7240  hashinfom  10645  shftfn  10717  phimullem  12088  ennnfonelemhom  12127  qnnen  12143  cldrcl  12473  neiss2  12513  txdis1cn  12649