Theorem fndm 5436

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4731  Fun wfun 5327   Fn wfn 5328

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 5336

This theorem is referenced by:  fndmi  5437  fndmd  5438  funfni  5439  fndmu  5440  fnbr  5441  fnco  5447  fnresdm  5448  fnresdisj  5449  fnssresb  5451  fn0  5459  fnimadisj  5460  fnimaeq0  5461  dmmpti  5469  fdm  5495  f1dm  5556  f1odm  5596  f1o00  5629  fvelimab  5711  fvun1  5721  eqfnfv2  5754  fndmdif  5761  fneqeql2  5765  elpreima  5775  fsn2  5829  fncofn  5840  fconst3m  5881  fconst4m  5882  fnfvima  5899  funiunfvdm  5914  fnunirn  5918  dff13  5919  f1eqcocnv  5942  oprssov  6174  offval  6252  ofrfval  6253  fnexALT  6282  dmmpo  6378  dmmpoga  6382  suppvalfng  6418  suppvalfn  6419  suppfnss  6435  tposfo2  6476  smodm2  6504  smoel2  6512  tfrlem5  6523  tfrlem8  6527  tfrlem9  6528  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfrexlem  6543  tfri2d  6545  tfr1onlemsucaccv  6550  tfr1onlemubacc  6555  tfrcllemsucaccv  6563  tfri2  6575  rdgivallem  6590  ixpprc  6931  ixpssmap2g  6939  ixpssmapg  6940  bren  6960  fndmeng  7028  caseinl  7333  caseinr  7334  cc2lem  7528  dmaddpi  7588  dmmulpi  7589  hashinfom  11086  shftfn  11447  phimullem  12860  ennnfonelemhom  13099  qnnen  13115  fnpr2ob  13486  cldrcl  14896  neiss2  14936  txdis1cn  15072  uhgrm  16002  upgrfnen  16022  upgrex  16027  umgrfnen  16032