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

Theorem f1of1 6174
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 5933 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 475 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925
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 197  df-an 385  df-f1o 5933
This theorem is referenced by:  f1of  6175  f1sng  6216  f1oresrab  6435  f1prex  6579  f1ocnvfvrneq  6581  isof1oidb  6614  isores3  6625  isoini2  6629  isosolem  6637  f1oiso  6641  weniso  6644  weisoeq  6645  f1opw2  6930  f1ovv  7179  tposf12  7422  oacomf1olem  7689  enssdom  8022  domssex2  8161  mapen  8165  ssenen  8175  phplem4  8183  php3  8187  sucdom2  8197  ssfi  8221  f1finf1o  8228  domunfican  8274  fiint  8278  f1opwfi  8311  mapfienlem1  8351  mapfienlem2  8352  mapfien  8354  marypha1lem  8380  ordtypelem10  8473  oiexg  8481  unxpwdom2  8534  wemapwe  8632  isinffi  8856  infxpenlem  8874  fseqenlem1  8885  dfac12lem2  9004  dfac12r  9006  ackbij2  9103  cff1  9118  infpssrlem4  9166  fin4en1  9169  enfin2i  9181  fin23lem28  9200  isf32lem7  9219  isf34lem3  9235  enfin1ai  9244  canthnum  9509  canthwe  9511  canthp1lem2  9513  pwfseqlem4  9522  pwfseqlem5  9523  tskuni  9643  grothomex  9689  negfi  11009  seqf1olem1  12880  hashfacen  13276  hashf1lem1  13277  fsumss  14500  ackbijnn  14604  fprodss  14722  bitsinv2  15212  bitsf1  15215  sadasslem  15239  sadeq  15241  phimullem  15531  eulerthlem2  15534  unbenlem  15659  f1ocpbllem  16231  f1ovscpbl  16233  xpsff1o2  16278  xpsmnd  17377  xpsgrp  17581  eqgen  17694  conjsubgen  17740  subggim  17755  gicsubgen  17767  symgfvne  17854  symgextf1  17887  symgfixelsi  17901  f1omvdmvd  17909  f1omvdconj  17912  pmtrfconj  17932  odngen  18038  sylow1lem2  18060  sylow2blem1  18081  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  dprdf1o  18477  rim0to0  18790  coe1sfi  19631  coe1mul2lem2  19686  gsumfsum  19861  zntoslem  19953  znunithash  19961  iporthcom  20028  lindfres  20210  islindf3  20213  lindsmm  20215  lmimlbs  20223  lbslcic  20228  resthauslem  21215  sshauslem  21224  basqtop  21562  tgqtop  21563  hmeoopn  21617  hmeocld  21618  hmeontr  21620  hmeoimaf1o  21621  haushmphlem  21638  tsmsf1o  21995  imasdsf1olem  22225  imasf1oxmet  22227  imasf1oxms  22341  ovoliunlem1  23316  dyadmbl  23414  vitalilem3  23424  dvcnvlem  23784  dvne0f1  23820  dvcnvrelem2  23826  logf1o2  24441  dvlog  24442  wilthlem3  24841  istrkg2ld  25404  f1otrg  25796  axcontlem10  25898  usgrf1  26112  usgrexmplef  26196  usgrres1  26252  edgusgrnbfin  26319  usgrexilem  26392  sizusglecusglem1  26413  uspgr2wlkeq  26598  trlres  26653  usgr2trlncl  26712  clwlkclwwlk  26968  adjbd1o  29072  padct  29625  madjusmdetlem4  30024  tpr2rico  30086  qqhre  30192  indf1ofs  30216  eulerpartgbij  30562  eulerpartlemgh  30568  ballotlemscr  30708  ballotlemro  30712  ballotlemfrc  30716  ballotlemrinv0  30722  reprpmtf1o  30832  derangenlem  31279  subfacp1lem3  31290  subfacp1lem5  31292  erdsze2lem1  31311  cvmliftmolem1  31389  cvmlift2lem9a  31411  phpreu  33523  poimirlem1  33540  poimirlem4  33543  poimirlem9  33548  poimirlem22  33561  mblfinlem2  33577  metf1o  33681  ismtyima  33732  ismtyres  33737  rngoisocnv  33910  laut11  35690  diaf1oN  36736  mapdcnvcl  37258  mapdcnvid2  37263  eldioph2lem2  37641  eldioph2  37642  pwfi2f1o  37983  gicabl  37986  sge0f1o  40917  nnfoctbdjlem  40990
  Copyright terms: Public domain W3C validator