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

Theorem f1odm 5650
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 5647 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5515 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   dom cdm 4845    Fn wfn 5418   -1-1-onto->wf1o 5422
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 185  df-an 371  df-fn 5426  df-f 5427  df-f1 5428  df-f1o 5430
This theorem is referenced by:  f1imacnv  5662  f1opw2  6318  xpcomco  7406  domss2  7475  mapen  7480  ssenen  7490  phplem4  7498  php3  7502  f1opwfi  7620  unxpwdom2  7808  cnfcomlem  7937  cnfcomlemOLD  7945  ackbij2lem2  8414  ackbij2lem3  8415  fin4en1  8483  enfin2i  8495  hashfacen  12212  ackbijnn  13296  gsumpropd2lem  15510  symgbas  15890  symgfixf1  15948  f1omvdmvd  15954  f1omvdconj  15957  pmtrfb  15976  symggen  15981  symggen2  15982  psgnunilem1  16004  psgnghm2  18016  basqtop  19289  reghmph  19371  nrmhmph  19372  indishmph  19376  ordthmeolem  19379  ufldom  19540  tgpconcompeqg  19687  imasf1oxms  20069  icchmeo  20518  dvcvx  21497  dvloglem  22098  tpr2rico  26347  ballotlemrv  26907  subfacp1lem2b  27074  subfacp1lem5  27077  ismtyres  28712  eldioph2lem1  29103  lnmlmic  29446
  Copyright terms: Public domain W3C validator