ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fdm Unicode version

Theorem fdm 5166
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fdm  |-  ( F : A --> B  ->  dom  F  =  A )

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5161 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5113 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 14 1  |-  ( F : A --> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289   dom cdm 4438    Fn wfn 5010   -->wf 5011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-fn 5018  df-f 5019
This theorem is referenced by:  fdmd  5167  fdmi  5168  fssxp  5178  ffdm  5181  dmfex  5200  f00  5202  f0dom0  5204  f0rn0  5205  foima  5238  foco  5243  resdif  5275  fimacnv  5428  dff3im  5444  ffvresb  5461  resflem  5462  fmptco  5464  fornex  5886  issmo2  6054  smoiso  6067  tfrcllemubacc  6124  rdgon  6151  frecabcl  6164  frecsuclem  6171  mapprc  6409  elpm2r  6423  map0b  6444  mapsn  6447  brdomg  6465  fopwdom  6552  casef  6779  nn0supp  8725  frecuzrdgdomlem  9824  frecuzrdgsuctlem  9830  zfz1isolemiso  10244  nninfall  11900
  Copyright terms: Public domain W3C validator