Theorem fndm 5316

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

Syntax hints:   → wi 4   = wceq 1353  dom cdm 4627  Fun wfun 5211   Fn wfn 5212

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 5220

This theorem is referenced by:  funfni  5317  fndmu  5318  fnbr  5319  fnco  5325  fnresdm  5326  fnresdisj  5327  fnssresb  5329  fn0  5336  fnimadisj  5337  fnimaeq0  5338  dmmpti  5346  fdm  5372  f1dm  5427  f1odm  5466  f1o00  5497  fvelimab  5573  fvun1  5583  eqfnfv2  5615  fndmdif  5622  fneqeql2  5626  elpreima  5636  fsn2  5691  fconst3m  5736  fconst4m  5737  fnfvima  5752  funiunfvdm  5764  fnunirn  5768  dff13  5769  f1eqcocnv  5792  oprssov  6016  offval  6090  ofrfval  6091  fnexALT  6112  dmmpo  6206  dmmpoga  6209  tposfo2  6268  smodm2  6296  smoel2  6304  tfrlem5  6315  tfrlem8  6319  tfrlem9  6320  tfrlemisucaccv  6326  tfrlemiubacc  6331  tfrexlem  6335  tfri2d  6337  tfr1onlemsucaccv  6342  tfr1onlemubacc  6347  tfrcllemsucaccv  6355  tfri2  6367  rdgivallem  6382  ixpprc  6719  ixpssmap2g  6727  ixpssmapg  6728  bren  6747  fndmeng  6810  caseinl  7090  caseinr  7091  cc2lem  7265  dmaddpi  7324  dmmulpi  7325  hashinfom  10758  shftfn  10833  phimullem  12225  ennnfonelemhom  12416  qnnen  12432  fnpr2ob  12759  cldrcl  13605  neiss2  13645  txdis1cn  13781