Theorem fndm 5372

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

Syntax hints:   → wi 4   = wceq 1372  dom cdm 4674  Fun wfun 5264   Fn wfn 5265

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 5273

This theorem is referenced by:  fndmi  5373  fndmd  5374  funfni  5375  fndmu  5376  fnbr  5377  fnco  5383  fnresdm  5384  fnresdisj  5385  fnssresb  5387  fn0  5394  fnimadisj  5395  fnimaeq0  5396  dmmpti  5404  fdm  5430  f1dm  5485  f1odm  5525  f1o00  5556  fvelimab  5634  fvun1  5644  eqfnfv2  5677  fndmdif  5684  fneqeql2  5688  elpreima  5698  fsn2  5753  fconst3m  5802  fconst4m  5803  fnfvima  5818  funiunfvdm  5831  fnunirn  5835  dff13  5836  f1eqcocnv  5859  oprssov  6087  offval  6165  ofrfval  6166  fnexALT  6195  dmmpo  6289  dmmpoga  6293  tposfo2  6352  smodm2  6380  smoel2  6388  tfrlem5  6399  tfrlem8  6403  tfrlem9  6404  tfrlemisucaccv  6410  tfrlemiubacc  6415  tfrexlem  6419  tfri2d  6421  tfr1onlemsucaccv  6426  tfr1onlemubacc  6431  tfrcllemsucaccv  6439  tfri2  6451  rdgivallem  6466  ixpprc  6805  ixpssmap2g  6813  ixpssmapg  6814  bren  6834  fndmeng  6901  caseinl  7192  caseinr  7193  cc2lem  7377  dmaddpi  7437  dmmulpi  7438  hashinfom  10921  shftfn  11077  phimullem  12489  ennnfonelemhom  12728  qnnen  12744  fnpr2ob  13114  cldrcl  14516  neiss2  14556  txdis1cn  14692