Theorem fndm 5429

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

Syntax hints:   → wi 4   = wceq 1397  dom cdm 4725  Fun wfun 5320   Fn wfn 5321

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 5329

This theorem is referenced by:  fndmi  5430  fndmd  5431  funfni  5432  fndmu  5433  fnbr  5434  fnco  5440  fnresdm  5441  fnresdisj  5442  fnssresb  5444  fn0  5452  fnimadisj  5453  fnimaeq0  5454  dmmpti  5462  fdm  5488  f1dm  5547  f1odm  5587  f1o00  5620  fvelimab  5702  fvun1  5712  eqfnfv2  5745  fndmdif  5752  fneqeql2  5756  elpreima  5766  fsn2  5821  fncofn  5831  fconst3m  5872  fconst4m  5873  fnfvima  5888  funiunfvdm  5903  fnunirn  5907  dff13  5908  f1eqcocnv  5931  oprssov  6163  offval  6242  ofrfval  6243  fnexALT  6272  dmmpo  6368  dmmpoga  6372  tposfo2  6432  smodm2  6460  smoel2  6468  tfrlem5  6479  tfrlem8  6483  tfrlem9  6484  tfrlemisucaccv  6490  tfrlemiubacc  6495  tfrexlem  6499  tfri2d  6501  tfr1onlemsucaccv  6506  tfr1onlemubacc  6511  tfrcllemsucaccv  6519  tfri2  6531  rdgivallem  6546  ixpprc  6887  ixpssmap2g  6895  ixpssmapg  6896  bren  6916  fndmeng  6984  caseinl  7289  caseinr  7290  cc2lem  7484  dmaddpi  7544  dmmulpi  7545  hashinfom  11039  shftfn  11384  phimullem  12796  ennnfonelemhom  13035  qnnen  13051  fnpr2ob  13422  cldrcl  14825  neiss2  14865  txdis1cn  15001  uhgrm  15928  upgrfnen  15948  upgrex  15953  umgrfnen  15958