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

Theorem f1odm 5525
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 5522 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5372 . 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 1372   dom cdm 4674    Fn wfn 5265   -1-1-onto->wf1o 5269
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 5273  df-f 5274  df-f1 5275  df-f1o 5277
This theorem is referenced by:  f1imacnv  5538  f1opw2  6151  en2  6911  xpcomco  6920  mapen  6942  ssenen  6947  phplem4  6951  phplem4on  6963  dif1en  6975  fiintim  7027  caseinl  7192  caseinr  7193  ctssdccl  7212  fihasheqf1oi  10930  hashfacen  10979  fisumss  11674
  Copyright terms: Public domain W3C validator