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

Theorem f1odm 5526
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 5523 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5373 . 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 1373   dom cdm 4675    Fn wfn 5266   -1-1-onto->wf1o 5270
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 5274  df-f 5275  df-f1 5276  df-f1o 5278
This theorem is referenced by:  f1imacnv  5539  f1opw2  6152  en2  6912  xpcomco  6921  mapen  6943  ssenen  6948  phplem4  6952  phplem4on  6964  dif1en  6976  fiintim  7028  caseinl  7193  caseinr  7194  ctssdccl  7213  fihasheqf1oi  10932  hashfacen  10981  fisumss  11703
  Copyright terms: Public domain W3C validator