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  5832  fconst3m  5873  fconst4m  5874  fnfvima  5889  funiunfvdm  5904  fnunirn  5908  dff13  5909  f1eqcocnv  5932  oprssov  6164  offval  6243  ofrfval  6244  fnexALT  6273  dmmpo  6369  dmmpoga  6373  tposfo2  6433  smodm2  6461  smoel2  6469  tfrlem5  6480  tfrlem8  6484  tfrlem9  6485  tfrlemisucaccv  6491  tfrlemiubacc  6496  tfrexlem  6500  tfri2d  6502  tfr1onlemsucaccv  6507  tfr1onlemubacc  6512  tfrcllemsucaccv  6520  tfri2  6532  rdgivallem  6547  ixpprc  6888  ixpssmap2g  6896  ixpssmapg  6897  bren  6917  fndmeng  6985  caseinl  7290  caseinr  7291  cc2lem  7485  dmaddpi  7545  dmmulpi  7546  hashinfom  11040  shftfn  11385  phimullem  12798  ennnfonelemhom  13037  qnnen  13053  fnpr2ob  13424  cldrcl  14828  neiss2  14868  txdis1cn  15004  uhgrm  15931  upgrfnen  15951  upgrex  15956  umgrfnen  15961