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

Theorem f1odm 5492
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 5489 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5359 . 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 1632   dom cdm 4705    Fn wfn 5266   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1imacnv  5505  f1opw2  6087  xpcomco  6968  domss2  7036  mapen  7041  ssenen  7051  phplem4  7059  php3  7063  f1opwfi  7175  unxpwdom2  7318  cnfcomlem  7418  ackbij2lem2  7882  ackbij2lem3  7883  fin4en1  7951  enfin2i  7963  hashfacen  11408  ackbijnn  12302  symgbas  14788  basqtop  17418  reghmph  17500  nrmhmph  17501  indishmph  17505  ordthmeolem  17508  ufldom  17673  tgpconcompeqg  17810  imasf1oxms  18051  icchmeo  18455  dvcvx  19383  dvloglem  20011  ballotlemrv  23094  tpr2rico  23311  gsumpropd2lem  23394  subfacp1lem2b  23727  subfacp1lem5  23730  ismtyres  26635  eldioph2lem1  26942  lnmlmic  27289  f1omvdmvd  27489  f1omvdconj  27492  pmtrfb  27509  symggen  27514  symggen2  27515  psgnunilem1  27519  psgnghm2  27541
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 5274  df-f 5275  df-f1 5276  df-f1o 5278
  Copyright terms: Public domain W3C validator