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

Theorem f1of1 5820
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of1

Proof of Theorem f1of1
StepHypRef Expression
1 df-f1o 5600 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592
This theorem is referenced by:  f1of  5821  f1oresrab  6063  f1ocnvfvrneq  6189  isores3  6231  isoini2  6235  isosolem  6243  f1oiso  6247  weniso  6250  weisoeq  6251  f1opw2  6528  f1ovv  6771  tposf12  6999  oacomf1olem  7232  enssdom  7560  domssex2  7697  mapen  7701  ssenen  7711  phplem4  7719  php3  7723  sucdom2  7734  ssfi  7760  f1finf1o  7766  domunfican  7813  fiint  7817  f1opwfi  7844  mapfienlem1  7884  mapfienlem2  7885  mapfien  7887  marypha1lem  7913  ordtypelem10  7973  oiexg  7981  unxpwdom2  8035  mapfienOLD  8159  wemapwe  8160  wemapweOLD  8161  isinffi  8394  infxpenlem  8412  fseqenlem1  8426  dfac12lem2  8545  dfac12r  8547  ackbij2  8644  cff1  8659  infpssrlem4  8707  fin4en1  8710  enfin2i  8722  fin23lem28  8741  isf32lem7  8760  isf34lem3  8776  enfin1ai  8785  canthnum  9048  canthwe  9050  canthp1lem2  9052  pwfseqlem4  9061  pwfseqlem5  9062  tskuni  9182  grothomex  9228  seqf1olem1  12146  hashfacen  12503  hashf1lem1  12504  fsumss  13547  ackbijnn  13640  fprodss  13755  bitsinv2  14093  bitsf1  14096  sadasslem  14120  sadeq  14122  phimullem  14309  eulerthlem2  14312  unbenlem  14426  f1ocpbllem  14921  f1ovscpbl  14923  xpsff1o2  14968  xpsmnd  15960  xpsgrp  16189  eqgen  16254  conjsubgen  16299  subggim  16314  gicsubgen  16326  symgfvne  16413  symgextf1  16446  symgfixelsi  16460  f1omvdmvd  16468  f1omvdconj  16471  pmtrfconj  16491  odngen  16597  sylow1lem2  16619  sylow2blem1  16640  gsumzres  16914  gsumzcl2  16915  gsumzf1o  16917  gsumzresOLD  16918  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  dprdf1o  17079  rim0to0  17391  coe1sfi  18252  coe1sfiOLD  18253  coe1mul2lem2  18309  gsumfsum  18484  zntoslem  18595  znunithash  18603  iporthcom  18670  lindfres  18858  islindf3  18861  lindsmm  18863  lmimlbs  18871  lbslcic  18876  resthauslem  19864  sshauslem  19873  basqtop  20212  tgqtop  20213  hmeoopn  20267  hmeocld  20268  hmeontr  20270  hmeoimaf1o  20271  haushmphlem  20288  tsmsf1o  20647  imasdsf1olem  20876  imasf1oxmet  20878  imasf1oxms  20992  ovoliunlem1  21913  dyadmbl  22009  vitalilem3  22019  dvcnvlem  22377  dvne0f1  22413  dvcnvrelem2  22419  logf1o2  23031  dvlog  23032  wilthlem3  23344  istrkg2ld  23858  f1otrg  24174  axcontlem10  24276  usgraf1  24360  uslgra1  24372  usgra1  24373  usgraexmpl  24401  edgusgranbfin  24450  cusgraexilem2  24467  sizeusglecusglem1  24484  2trllemE  24555  constr1trl  24590  usgra2adedgspthlem2  24612  constr3trllem2  24651  eupatrl  24968  eupares  24975  eupath2lem3  24979  adjbd1o  27004  tpr2rico  27894  qqhre  27998  indf1ofs  28039  eulerpartgbij  28311  eulerpartlemgh  28317  ballotlemscr  28457  ballotlemro  28461  ballotlemfrc  28465  ballotlemrinv0  28471  derangenlem  28615  subfacp1lem3  28626  subfacp1lem5  28628  erdsze2lem1  28647  cvmliftmolem1  28726  cvmlift2lem9a  28748  ghomf1olem  29034  mblfinlem2  30052  metf1o  30248  ismtyima  30299  ismtyres  30304  rngoisocnv  30384  eldioph2lem2  30694  eldioph2  30695  pwfi2f1o  31044  gicabl  31047  usgresvm1  32443  usgresvm1ALT  32447  laut11  35810  diaf1oN  36857  mapdcnvcl  37379  mapdcnvid2  37384
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-f1o 5600
  Copyright terms: Public domain W3C validator