Theorem fndm 5357

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

Syntax hints:   → wi 4   = wceq 1364  dom cdm 4663  Fun wfun 5252   Fn wfn 5253

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 5261

This theorem is referenced by:  funfni  5358  fndmu  5359  fnbr  5360  fnco  5366  fnresdm  5367  fnresdisj  5368  fnssresb  5370  fn0  5377  fnimadisj  5378  fnimaeq0  5379  dmmpti  5387  fdm  5413  f1dm  5468  f1odm  5508  f1o00  5539  fvelimab  5617  fvun1  5627  eqfnfv2  5660  fndmdif  5667  fneqeql2  5671  elpreima  5681  fsn2  5736  fconst3m  5781  fconst4m  5782  fnfvima  5797  funiunfvdm  5810  fnunirn  5814  dff13  5815  f1eqcocnv  5838  oprssov  6065  offval  6143  ofrfval  6144  fnexALT  6168  dmmpo  6262  dmmpoga  6266  tposfo2  6325  smodm2  6353  smoel2  6361  tfrlem5  6372  tfrlem8  6376  tfrlem9  6377  tfrlemisucaccv  6383  tfrlemiubacc  6388  tfrexlem  6392  tfri2d  6394  tfr1onlemsucaccv  6399  tfr1onlemubacc  6404  tfrcllemsucaccv  6412  tfri2  6424  rdgivallem  6439  ixpprc  6778  ixpssmap2g  6786  ixpssmapg  6787  bren  6806  fndmeng  6869  caseinl  7157  caseinr  7158  cc2lem  7333  dmaddpi  7392  dmmulpi  7393  hashinfom  10870  shftfn  10989  phimullem  12393  ennnfonelemhom  12632  qnnen  12648  fnpr2ob  12983  cldrcl  14338  neiss2  14378  txdis1cn  14514