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

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

Proof of Theorem f1of1
StepHypRef Expression
1 df-f1o 6357 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 500 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 6347  ontowfo 6348  1-1-ontowf1o 6349
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 209  df-an 399  df-f1o 6357
This theorem is referenced by:  f1of  6610  f1sng  6651  f1oresrab  6884  f1prex  7034  f1ocnvfvrneq  7036  isof1oidb  7071  isores3  7082  isoini2  7086  isosolem  7094  f1oiso  7098  weniso  7101  weisoeq  7102  f1opw2  7394  f1ovv  7653  tposf12  7911  oacomf1olem  8184  enssdom  8528  domssex2  8671  mapen  8675  ssenen  8685  phplem4  8693  php3  8697  sucdom2  8708  ssfi  8732  f1finf1o  8739  domunfican  8785  fiint  8789  f1opwfi  8822  mapfienlem1  8862  mapfienlem2  8863  mapfien  8865  marypha1lem  8891  ordtypelem10  8985  oiexg  8993  unxpwdom2  9046  wemapwe  9154  inlresf1  9338  inrresf1  9340  isinffi  9415  infxpenlem  9433  fseqenlem1  9444  dfac12lem2  9564  dfac12r  9566  ackbij2  9659  cff1  9674  infpssrlem4  9722  fin4en1  9725  enfin2i  9737  fin23lem28  9756  isf32lem7  9775  isf34lem3  9791  enfin1ai  9800  canthnum  10065  canthwe  10067  canthp1lem2  10069  pwfseqlem4  10078  pwfseqlem5  10079  tskuni  10199  grothomex  10245  negfi  11583  seqf1olem1  13403  hashfacen  13806  hashf1lem1  13807  fsumss  15076  ackbijnn  15177  fprodss  15296  bitsinv2  15786  bitsf1  15789  sadasslem  15813  sadeq  15815  phimullem  16110  eulerthlem2  16113  unbenlem  16238  f1ocpbllem  16791  f1ovscpbl  16793  xpsff1o2  16836  xpsmnd  17945  injsubmefmnd  18056  xpsgrp  18212  eqgen  18327  conjsubgen  18385  subggim  18400  gicsubgen  18412  symgfvne  18503  symgextf1  18543  symgfixelsi  18557  f1omvdmvd  18565  f1omvdconj  18568  pmtrfconj  18588  odngen  18696  sylow1lem2  18718  sylow2blem1  18739  gsumzres  19023  gsumzcl2  19024  gsumzf1o  19026  gsumzaddlem  19035  gsumconst  19048  gsumzmhm  19051  gsumzoppg  19058  dprdf1o  19148  gim0to0  19489  rim0to0OLD  19490  coe1sfi  20375  coe1mul2lem2  20430  gsumfsum  20606  zntoslem  20697  znunithash  20705  iporthcom  20773  lindfres  20961  islindf3  20964  lindsmm  20966  lmimlbs  20974  lbslcic  20979  resthauslem  21965  sshauslem  21974  basqtop  22313  tgqtop  22314  hmeoopn  22368  hmeocld  22369  hmeontr  22371  hmeoimaf1o  22372  haushmphlem  22389  tsmsf1o  22747  imasdsf1olem  22977  imasf1oxmet  22979  imasf1oxms  23093  ovoliunlem1  24097  dyadmbl  24195  vitalilem3  24205  dvcnvlem  24567  dvne0f1  24603  dvcnvrelem2  24609  logf1o2  25227  dvlog  25228  wilthlem3  25641  istrkg2ld  26240  f1otrg  26651  axcontlem10  26753  usgrf1  26951  usgrexmplef  27035  usgrres1  27091  edgusgrnbfin  27149  usgrexilem  27216  sizusglecusglem1  27237  uspgr2wlkeq  27421  trlres  27476  usgr2trlncl  27535  clwlkclwwlk  27774  adjbd1o  29856  padct  30449  s1f1  30614  s2f1  30616  cycpmconjv  30779  madjusmdetlem4  31090  tpr2rico  31150  qqhre  31256  indf1ofs  31280  eulerpartgbij  31625  eulerpartlemgh  31631  ballotlemscr  31771  ballotlemro  31775  ballotlemfrc  31779  ballotlemrinv0  31785  reprpmtf1o  31892  derangenlem  32413  subfacp1lem3  32424  subfacp1lem5  32426  erdsze2lem1  32445  cvmliftmolem1  32523  cvmlift2lem9a  32545  phpreu  34870  poimirlem1  34887  poimirlem4  34890  poimirlem9  34895  poimirlem22  34908  mblfinlem2  34924  metf1o  35024  ismtyima  35075  ismtyres  35080  rngoisocnv  35253  laut11  37216  diaf1oN  38260  mapdcnvcl  38782  mapdcnvid2  38787  eldioph2lem2  39351  eldioph2  39352  pwfi2f1o  39689  gicabl  39692  sge0f1o  42657  nnfoctbdjlem  42730  f1oresf1o  43482  fundcmpsurbijinjpreimafv  43560  fundcmpsurinjpreimafv  43561  fundcmpsurinjimaid  43564  isomuspgrlem1  43985  isomuspgrlem2c  43988  isomgrsym  43994
  Copyright terms: Public domain W3C validator