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

Theorem f1odm 5364
Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.)
Assertion
Ref Expression
f1odm  |-  ( F : A -1-1-onto-> B  ->  dom  F  =  A )

Proof of Theorem f1odm
StepHypRef Expression
1 f1ofn 5361 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5217 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 14 1  |-  ( F : A -1-1-onto-> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331   dom cdm 4534    Fn wfn 5113   -1-1-onto->wf1o 5117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-fn 5121  df-f 5122  df-f1 5123  df-f1o 5125
This theorem is referenced by:  f1imacnv  5377  f1opw2  5969  xpcomco  6713  mapen  6733  ssenen  6738  phplem4  6742  phplem4on  6754  dif1en  6766  fiintim  6810  caseinl  6969  caseinr  6970  ctssdccl  6989  fihasheqf1oi  10527  hashfacen  10572  fisumss  11154
  Copyright terms: Public domain W3C validator