Theorem fndm 5358

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

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

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 5262

This theorem is referenced by:  fndmi  5359  fndmd  5360  funfni  5361  fndmu  5362  fnbr  5363  fnco  5369  fnresdm  5370  fnresdisj  5371  fnssresb  5373  fn0  5380  fnimadisj  5381  fnimaeq0  5382  dmmpti  5390  fdm  5416  f1dm  5471  f1odm  5511  f1o00  5542  fvelimab  5620  fvun1  5630  eqfnfv2  5663  fndmdif  5670  fneqeql2  5674  elpreima  5684  fsn2  5739  fconst3m  5784  fconst4m  5785  fnfvima  5800  funiunfvdm  5813  fnunirn  5817  dff13  5818  f1eqcocnv  5841  oprssov  6069  offval  6147  ofrfval  6148  fnexALT  6177  dmmpo  6271  dmmpoga  6275  tposfo2  6334  smodm2  6362  smoel2  6370  tfrlem5  6381  tfrlem8  6385  tfrlem9  6386  tfrlemisucaccv  6392  tfrlemiubacc  6397  tfrexlem  6401  tfri2d  6403  tfr1onlemsucaccv  6408  tfr1onlemubacc  6413  tfrcllemsucaccv  6421  tfri2  6433  rdgivallem  6448  ixpprc  6787  ixpssmap2g  6795  ixpssmapg  6796  bren  6815  fndmeng  6878  caseinl  7166  caseinr  7167  cc2lem  7351  dmaddpi  7411  dmmulpi  7412  hashinfom  10889  shftfn  11008  phimullem  12420  ennnfonelemhom  12659  qnnen  12675  fnpr2ob  13044  cldrcl  14446  neiss2  14486  txdis1cn  14622