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

Theorem fdm 5119
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 5114 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5066 . 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 1285   dom cdm 4401    Fn wfn 4964   -->wf 4965
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 4972  df-f 4973
This theorem is referenced by:  fdmi  5120  fssxp  5127  ffdm  5130  dmfex  5148  f00  5150  f0dom0  5152  f0rn0  5153  foima  5186  foco  5191  resdif  5223  fimacnv  5373  dff3im  5389  ffvresb  5403  resflem  5404  fmptco  5406  fornex  5821  issmo2  5986  smoiso  5999  tfrcllemubacc  6056  rdgon  6083  frecabcl  6096  frecsuclem  6103  mapprc  6339  elpm2r  6353  map0b  6374  mapsn  6377  brdomg  6395  fopwdom  6482  casef  6686  nn0supp  8617  frecuzrdgdomlem  9713  frecuzrdgsuctlem  9719  nninfall  11241
  Copyright terms: Public domain W3C validator