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

Theorem f1of1 6031
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 5794 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 474 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  1-1wf1 5784  ontowfo 5785  1-1-ontowf1o 5786
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 195  df-an 384  df-f1o 5794
This theorem is referenced by:  f1of  6032  f1sng  6072  f1oresrab  6284  f1prex  6414  f1ocnvfvrneq  6416  isof1oidb  6449  isores3  6460  isoini2  6464  isosolem  6472  f1oiso  6476  weniso  6479  weisoeq  6480  f1opw2  6760  f1ovv  7004  tposf12  7238  oacomf1olem  7505  enssdom  7840  domssex2  7979  mapen  7983  ssenen  7993  phplem4  8001  php3  8005  sucdom2  8015  ssfi  8039  f1finf1o  8046  domunfican  8092  fiint  8096  f1opwfi  8127  mapfienlem1  8167  mapfienlem2  8168  mapfien  8170  marypha1lem  8196  ordtypelem10  8289  oiexg  8297  unxpwdom2  8350  wemapwe  8451  isinffi  8675  infxpenlem  8693  fseqenlem1  8704  dfac12lem2  8823  dfac12r  8825  ackbij2  8922  cff1  8937  infpssrlem4  8985  fin4en1  8988  enfin2i  9000  fin23lem28  9019  isf32lem7  9038  isf34lem3  9054  enfin1ai  9063  canthnum  9324  canthwe  9326  canthp1lem2  9328  pwfseqlem4  9337  pwfseqlem5  9338  tskuni  9458  grothomex  9504  negfi  10817  seqf1olem1  12654  hashfacen  13044  hashf1lem1  13045  fsumss  14246  ackbijnn  14342  fprodss  14460  bitsinv2  14946  bitsf1  14949  sadasslem  14973  sadeq  14975  phimullem  15265  eulerthlem2  15268  unbenlem  15393  f1ocpbllem  15950  f1ovscpbl  15952  xpsff1o2  15997  xpsmnd  17096  xpsgrp  17300  eqgen  17413  conjsubgen  17459  subggim  17474  gicsubgen  17487  symgfvne  17574  symgextf1  17607  symgfixelsi  17621  f1omvdmvd  17629  f1omvdconj  17632  pmtrfconj  17652  odngen  17758  sylow1lem2  17780  sylow2blem1  17801  gsumzres  18076  gsumzcl2  18077  gsumzf1o  18079  gsumzaddlem  18087  gsumconst  18100  gsumzmhm  18103  gsumzoppg  18110  dprdf1o  18197  rim0to0  18508  coe1sfi  19347  coe1mul2lem2  19402  gsumfsum  19575  zntoslem  19666  znunithash  19674  iporthcom  19741  lindfres  19920  islindf3  19923  lindsmm  19925  lmimlbs  19933  lbslcic  19938  resthauslem  20916  sshauslem  20925  basqtop  21263  tgqtop  21264  hmeoopn  21318  hmeocld  21319  hmeontr  21321  hmeoimaf1o  21322  haushmphlem  21339  tsmsf1o  21697  imasdsf1olem  21926  imasf1oxmet  21928  imasf1oxms  22042  ovoliunlem1  22991  dyadmbl  23088  vitalilem3  23099  dvcnvlem  23457  dvne0f1  23493  dvcnvrelem2  23499  logf1o2  24110  dvlog  24111  wilthlem3  24510  istrkg2ld  25073  f1otrg  25466  axcontlem10  25568  usgraf1  25652  uslgra1  25664  usgra1  25665  usgraexmplef  25692  edgusgranbfin  25742  cusgraexilem2  25759  sizeusglecusglem1  25775  2trllemE  25846  constr1trl  25881  usgra2adedgspthlem2  25903  constr3trllem2  25942  eupatrl  26258  eupares  26265  eupath2lem3  26269  adjbd1o  28131  padct  28688  madjusmdetlem4  29027  tpr2rico  29089  qqhre  29195  indf1ofs  29218  eulerpartgbij  29564  eulerpartlemgh  29570  ballotlemscr  29710  ballotlemro  29714  ballotlemfrc  29718  ballotlemrinv0  29724  derangenlem  30210  subfacp1lem3  30221  subfacp1lem5  30223  erdsze2lem1  30242  cvmliftmolem1  30320  cvmlift2lem9a  30342  phpreu  32363  poimirlem1  32380  poimirlem4  32383  poimirlem9  32388  poimirlem22  32401  mblfinlem2  32417  metf1o  32521  ismtyima  32572  ismtyres  32577  rngoisocnv  32750  laut11  34190  diaf1oN  35237  mapdcnvcl  35759  mapdcnvid2  35764  eldioph2lem2  36142  eldioph2  36143  pwfi2f1o  36484  gicabl  36487  sge0f1o  39076  nnfoctbdjlem  39149  usgrf1  40401  usgrres1  40533  edgusgrnbfin  40600  usgrexi  40660  sizusglecusglem1  40676  uspgr2wlkeq  40853  trlres  40907  usgr2trlncl  40965  clwlkclwwlk  41210
  Copyright terms: Public domain W3C validator