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

Theorem f1of1 6607
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 6355 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 498 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 6345  ontowfo 6346  1-1-ontowf1o 6347
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 208  df-an 397  df-f1o 6355
This theorem is referenced by:  f1of  6608  f1sng  6649  f1oresrab  6881  f1prex  7031  f1ocnvfvrneq  7033  isof1oidb  7066  isores3  7077  isoini2  7081  isosolem  7089  f1oiso  7093  weniso  7096  weisoeq  7097  f1opw2  7389  f1ovv  7648  tposf12  7906  oacomf1olem  8179  enssdom  8522  domssex2  8665  mapen  8669  ssenen  8679  phplem4  8687  php3  8691  sucdom2  8702  ssfi  8726  f1finf1o  8733  domunfican  8779  fiint  8783  f1opwfi  8816  mapfienlem1  8856  mapfienlem2  8857  mapfien  8859  marypha1lem  8885  ordtypelem10  8979  oiexg  8987  unxpwdom2  9040  wemapwe  9148  inlresf1  9332  inrresf1  9334  isinffi  9409  infxpenlem  9427  fseqenlem1  9438  dfac12lem2  9558  dfac12r  9560  ackbij2  9653  cff1  9668  infpssrlem4  9716  fin4en1  9719  enfin2i  9731  fin23lem28  9750  isf32lem7  9769  isf34lem3  9785  enfin1ai  9794  canthnum  10059  canthwe  10061  canthp1lem2  10063  pwfseqlem4  10072  pwfseqlem5  10073  tskuni  10193  grothomex  10239  negfi  11577  seqf1olem1  13397  hashfacen  13800  hashf1lem1  13801  fsumss  15070  ackbijnn  15171  fprodss  15290  bitsinv2  15780  bitsf1  15783  sadasslem  15807  sadeq  15809  phimullem  16104  eulerthlem2  16107  unbenlem  16232  f1ocpbllem  16785  f1ovscpbl  16787  xpsff1o2  16830  xpsmnd  17939  xpsgrp  18156  eqgen  18271  conjsubgen  18329  subggim  18344  gicsubgen  18356  symgfvne  18444  symgextf1  18478  symgfixelsi  18492  f1omvdmvd  18500  f1omvdconj  18503  pmtrfconj  18523  odngen  18631  sylow1lem2  18653  sylow2blem1  18674  gsumzres  18958  gsumzcl2  18959  gsumzf1o  18961  gsumzaddlem  18970  gsumconst  18983  gsumzmhm  18986  gsumzoppg  18993  dprdf1o  19083  gim0to0  19424  rim0to0OLD  19425  coe1sfi  20309  coe1mul2lem2  20364  gsumfsum  20540  zntoslem  20631  znunithash  20639  iporthcom  20707  lindfres  20895  islindf3  20898  lindsmm  20900  lmimlbs  20908  lbslcic  20913  resthauslem  21899  sshauslem  21908  basqtop  22247  tgqtop  22248  hmeoopn  22302  hmeocld  22303  hmeontr  22305  hmeoimaf1o  22306  haushmphlem  22323  tsmsf1o  22680  imasdsf1olem  22910  imasf1oxmet  22912  imasf1oxms  23026  ovoliunlem1  24030  dyadmbl  24128  vitalilem3  24138  dvcnvlem  24500  dvne0f1  24536  dvcnvrelem2  24542  logf1o2  25160  dvlog  25161  wilthlem3  25574  istrkg2ld  26173  f1otrg  26584  axcontlem10  26686  usgrf1  26884  usgrexmplef  26968  usgrres1  27024  edgusgrnbfin  27082  usgrexilem  27149  sizusglecusglem1  27170  uspgr2wlkeq  27354  trlres  27409  usgr2trlncl  27468  clwlkclwwlk  27707  adjbd1o  29789  padct  30381  s1f1  30546  s2f1  30548  cycpmconjv  30711  madjusmdetlem4  30994  tpr2rico  31054  qqhre  31160  indf1ofs  31184  eulerpartgbij  31529  eulerpartlemgh  31535  ballotlemscr  31675  ballotlemro  31679  ballotlemfrc  31683  ballotlemrinv0  31689  reprpmtf1o  31796  derangenlem  32315  subfacp1lem3  32326  subfacp1lem5  32328  erdsze2lem1  32347  cvmliftmolem1  32425  cvmlift2lem9a  32447  phpreu  34757  poimirlem1  34774  poimirlem4  34777  poimirlem9  34782  poimirlem22  34795  mblfinlem2  34811  metf1o  34911  ismtyima  34962  ismtyres  34967  rngoisocnv  35140  laut11  37102  diaf1oN  38146  mapdcnvcl  38668  mapdcnvid2  38673  eldioph2lem2  39236  eldioph2  39237  pwfi2f1o  39574  gicabl  39577  sge0f1o  42541  nnfoctbdjlem  42614  f1oresf1o  43366  fundcmpsurbijinjpreimafv  43444  fundcmpsurinjpreimafv  43445  fundcmpsurinjimaid  43448  isomuspgrlem1  43869  isomuspgrlem2c  43872  isomgrsym  43878  injsubmefmnd  43994
  Copyright terms: Public domain W3C validator