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

Theorem f1of1 5723
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )

Proof of Theorem f1of1
StepHypRef Expression
1 df-f1o 5503 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 458 1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   -1-1->wf1 5493   -onto->wfo 5494   -1-1-onto->wf1o 5495
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 369  df-f1o 5503
This theorem is referenced by:  f1of  5724  f1oresrab  5965  f1ocnvfvrneq  6090  isores3  6132  isoini2  6136  isosolem  6144  f1oiso  6148  weniso  6151  weisoeq  6152  f1opw2  6427  f1ovv  6670  tposf12  6898  oacomf1olem  7131  enssdom  7459  domssex2  7596  mapen  7600  ssenen  7610  phplem4  7618  php3  7622  sucdom2  7632  ssfi  7656  f1finf1o  7662  domunfican  7708  fiint  7712  f1opwfi  7739  mapfienlem1  7779  mapfienlem2  7780  mapfien  7782  marypha1lem  7808  ordtypelem10  7867  oiexg  7875  unxpwdom2  7929  mapfienOLD  8051  wemapwe  8052  wemapweOLD  8053  isinffi  8286  infxpenlem  8304  fseqenlem1  8318  dfac12lem2  8437  dfac12r  8439  ackbij2  8536  cff1  8551  infpssrlem4  8599  fin4en1  8602  enfin2i  8614  fin23lem28  8633  isf32lem7  8652  isf34lem3  8668  enfin1ai  8677  canthnum  8938  canthwe  8940  canthp1lem2  8942  pwfseqlem4  8951  pwfseqlem5  8952  tskuni  9072  grothomex  9118  seqf1olem1  12049  hashfacen  12407  hashf1lem1  12408  fsumss  13549  ackbijnn  13642  fprodss  13757  bitsinv2  14095  bitsf1  14098  sadasslem  14122  sadeq  14124  phimullem  14311  eulerthlem2  14314  unbenlem  14428  f1ocpbllem  14931  f1ovscpbl  14933  xpsff1o2  14978  xpsmnd  16077  xpsgrp  16306  eqgen  16371  conjsubgen  16416  subggim  16431  gicsubgen  16443  symgfvne  16530  symgextf1  16563  symgfixelsi  16577  f1omvdmvd  16585  f1omvdconj  16588  pmtrfconj  16608  odngen  16714  sylow1lem2  16736  sylow2blem1  16757  gsumzres  17031  gsumzcl2  17032  gsumzf1o  17034  gsumzresOLD  17035  gsumzclOLD  17036  gsumzf1oOLD  17037  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsumconst  17070  gsumzmhm  17073  gsumzmhmOLD  17074  gsumzoppg  17083  gsumzoppgOLD  17084  dprdf1o  17192  rim0to0  17504  coe1sfi  18365  coe1sfiOLD  18366  coe1mul2lem2  18422  gsumfsum  18597  zntoslem  18686  znunithash  18694  iporthcom  18761  lindfres  18943  islindf3  18946  lindsmm  18948  lmimlbs  18956  lbslcic  18961  resthauslem  19950  sshauslem  19959  basqtop  20297  tgqtop  20298  hmeoopn  20352  hmeocld  20353  hmeontr  20355  hmeoimaf1o  20356  haushmphlem  20373  tsmsf1o  20732  imasdsf1olem  20961  imasf1oxmet  20963  imasf1oxms  21077  ovoliunlem1  21998  dyadmbl  22094  vitalilem3  22104  dvcnvlem  22462  dvne0f1  22498  dvcnvrelem2  22504  logf1o2  23118  dvlog  23119  wilthlem3  23461  istrkg2ld  23975  f1otrg  24295  axcontlem10  24397  usgraf1  24481  uslgra1  24493  usgra1  24494  usgraexmpl  24522  edgusgranbfin  24571  cusgraexilem2  24588  sizeusglecusglem1  24605  2trllemE  24676  constr1trl  24711  usgra2adedgspthlem2  24733  constr3trllem2  24772  eupatrl  25089  eupares  25096  eupath2lem3  25100  adjbd1o  27120  padct  27695  tpr2rico  28048  qqhre  28151  indf1ofs  28174  eulerpartgbij  28494  eulerpartlemgh  28500  ballotlemscr  28640  ballotlemro  28644  ballotlemfrc  28648  ballotlemrinv0  28654  derangenlem  28804  subfacp1lem3  28815  subfacp1lem5  28817  erdsze2lem1  28836  cvmliftmolem1  28915  cvmlift2lem9a  28937  ghomf1olem  29223  mblfinlem2  30217  metf1o  30414  ismtyima  30465  ismtyres  30470  rngoisocnv  30550  eldioph2lem2  30859  eldioph2  30860  pwfi2f1o  31210  pwfi2f1oOLD  31211  gicabl  31215  usgresvm1  32761  usgresvm1ALT  32765  laut11  36223  diaf1oN  37270  mapdcnvcl  37792  mapdcnvid2  37797
  Copyright terms: Public domain W3C validator