MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1odm Unicode version

Theorem f1odm 5476
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 5473 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5343 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 15 1  |-  ( F : A -1-1-onto-> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   dom cdm 4689    Fn wfn 5250   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1imacnv  5489  f1opw2  6071  xpcomco  6952  domss2  7020  mapen  7025  ssenen  7035  phplem4  7043  php3  7047  f1opwfi  7159  unxpwdom2  7302  cnfcomlem  7402  ackbij2lem2  7866  ackbij2lem3  7867  fin4en1  7935  enfin2i  7947  hashfacen  11392  ackbijnn  12286  symgbas  14772  basqtop  17402  reghmph  17484  nrmhmph  17485  indishmph  17489  ordthmeolem  17492  ufldom  17657  tgpconcompeqg  17794  imasf1oxms  18035  icchmeo  18439  dvcvx  19367  dvloglem  19995  ballotlemrv  23078  tpr2rico  23296  gsumpropd2lem  23379  subfacp1lem2b  23712  subfacp1lem5  23715  ismtyres  26532  eldioph2lem1  26839  lnmlmic  27186  f1omvdmvd  27386  f1omvdconj  27389  pmtrfb  27406  symggen  27411  symggen2  27412  psgnunilem1  27416  psgnghm2  27438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5258  df-f 5259  df-f1 5260  df-f1o 5262
  Copyright terms: Public domain W3C validator