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

Theorem f1odm 5680
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 5677 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fndm 5546 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   dom cdm 4880    Fn wfn 5451   -1-1-onto->wf1o 5455
This theorem is referenced by:  f1imacnv  5693  f1opw2  6300  xpcomco  7200  domss2  7268  mapen  7273  ssenen  7283  phplem4  7291  php3  7295  f1opwfi  7412  unxpwdom2  7558  cnfcomlem  7658  ackbij2lem2  8122  ackbij2lem3  8123  fin4en1  8191  enfin2i  8203  hashfacen  11705  ackbijnn  12609  symgbas  15097  basqtop  17745  reghmph  17827  nrmhmph  17828  indishmph  17832  ordthmeolem  17835  ufldom  17996  tgpconcompeqg  18143  imasf1oxms  18521  icchmeo  18968  dvcvx  19906  dvloglem  20541  gsumpropd2lem  24222  tpr2rico  24312  ballotlemrv  24779  subfacp1lem2b  24869  subfacp1lem5  24872  ismtyres  26519  eldioph2lem1  26820  lnmlmic  27165  f1omvdmvd  27365  f1omvdconj  27368  pmtrfb  27385  symggen  27390  symggen2  27391  psgnunilem1  27395  psgnghm2  27417
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 179  df-an 362  df-fn 5459  df-f 5460  df-f1 5461  df-f1o 5463
  Copyright terms: Public domain W3C validator