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

Theorem f1odm 5840
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 5837 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5696 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 17 1  |-  ( F : A -1-1-onto-> B  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454   dom cdm 4852    Fn wfn 5595   -1-1-onto->wf1o 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190  df-an 377  df-fn 5603  df-f 5604  df-f1 5605  df-f1o 5607
This theorem is referenced by:  f1imacnv  5852  f1opw2  6548  xpcomco  7687  domss2  7756  mapen  7761  ssenen  7771  phplem4  7779  php3  7783  f1opwfi  7903  unxpwdom2  8128  cnfcomlem  8229  ackbij2lem2  8695  ackbij2lem3  8696  fin4en1  8764  enfin2i  8776  hashfacen  12649  gsumpropd2lem  16564  symgbas  17069  symgfixf1  17126  f1omvdmvd  17132  f1omvdconj  17135  pmtrfb  17154  symggen  17159  symggen2  17160  psgnunilem1  17182  basqtop  20774  reghmph  20856  nrmhmph  20857  indishmph  20861  ordthmeolem  20864  ufldom  21025  tgpconcompeqg  21174  imasf1oxms  21552  icchmeo  22017  dvcvx  23020  dvloglem  23641  f1ocnt  28424  madjusmdetlem2  28702  madjusmdetlem4  28704  tpr2rico  28766  ballotlemrv  29400  ballotlemrvOLD  29438  subfacp1lem2b  29952  subfacp1lem5  29955  poimirlem3  31987  ismtyres  32184  eldioph2lem1  35646  lnmlmic  35990  ssnnf1octb  37507
  Copyright terms: Public domain W3C validator