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

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

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 6607 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 6568 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wf 6344  1-1wf1 6345  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-f1 6353  df-f1o 6355
This theorem is referenced by:  f1ofn  6609  f1ompt  6867  f1oresrab  6881  fsn  6889  fsnunf  6939  f1ocnvfv1  7024  f1ocnvfv2  7025  fsnex  7030  f1ocnvdm  7032  fcof1oinvd  7040  fveqf1o  7049  isocnv  7072  isocnv3  7074  isores2  7075  isotr  7078  isofr2  7086  isopolem  7087  isosolem  7089  f1oiso2  7094  weniso  7096  f1ofveu  7140  f1oexrnex  7621  f1oabexg  7631  wemoiso  7663  suppsnop  7833  smoiso  7988  mapsnd  8438  ralxpmap  8448  f1oen2g  8514  en1  8564  enfixsn  8614  mapen  8669  ac6sfi  8750  domunfican  8779  fiint  8783  mapfienlem1  8856  mapfienlem2  8857  mapfienlem3  8858  mapfien  8859  supisoex  8926  supiso  8927  ordiso2  8967  ordtypelem10  8979  unxpwdom2  9040  cantnfle  9122  cantnfp1lem3  9131  cantnflem1b  9137  cantnflem1d  9139  cantnflem1  9140  cnfcomlem  9150  cnfcom  9151  cnfcom2lem  9152  cnfcom2  9153  cnfcom3lem  9154  cnfcom3  9155  cnfcom3clem  9156  djuin  9335  infxpenlem  9427  infxpenc  9432  infxpenc2lem2  9434  fseqenlem1  9438  acndom  9465  acndom2  9468  infpwfien  9476  iunfictbso  9528  infmap2  9628  ackbij2lem2  9650  infpssrlem3  9715  infpssrlem4  9716  fin23lem30  9752  isf32lem6  9768  isf32lem7  9769  isf32lem8  9770  enfin1ai  9794  axcc3  9848  axcclem  9867  ttukeylem7  9925  fpwwe2lem6  10045  fpwwe2lem7  10046  fpwwe2lem9  10048  canthp1lem2  10063  canthp1  10064  pwfseqlem4a  10071  pwfseqlem5  10073  axdc4uzlem  13339  seqf1olem1  13397  seqf1olem2  13398  seqf1o  13399  hashkf  13680  hasheqf1oi  13700  hasheqf1od  13702  hashcl  13705  hashgadd  13726  hashfacen  13800  hashf1lem1  13801  fz1isolem  13807  seqcoll  13810  seqcoll2  13811  cnrecnv  14512  sumeq2ii  15038  summolem3  15059  summolem2a  15060  fsum  15065  fsumf1o  15068  fsumss  15070  fsumcl2lem  15076  fsumadd  15084  fsummulc2  15127  fsumrelem  15150  ackbijnn  15171  prodeq2ii  15255  prodmolem3  15275  prodmolem2a  15276  fprod  15283  fprodf1o  15288  fprodss  15290  fprodser  15291  fprodcl2lem  15292  fprodmul  15302  fproddiv  15303  fprodn0  15321  fproddvdsd  15672  sadcaddlem  15794  sadadd2lem  15796  sadadd3  15798  sadaddlem  15803  sadasslem  15807  sadeq  15809  phimullem  16104  eulerthlem1  16106  eulerthlem2  16107  unbenlem  16232  vdwlem8  16312  0ram  16344  wunndx  16492  xpsaddlem  16834  xpsvsca  16838  xpsle  16840  idfucl  17139  setccatid  17332  setcinv  17338  catcisolem  17354  estrccatid  17370  funcestrcsetclem7  17384  funcestrcsetclem8  17385  funcsetcestrclem7  17399  funcsetcestrclem8  17400  yonffthlem  17520  gsumpropd2lem  17877  idmhm  17953  mhmf1o  17954  gsumws1  17990  idghm  18311  ghmf1o  18326  symgval  18435  symgbas  18436  elsymgbas  18438  symgbasf  18440  symgbasfi  18442  symg1bas  18453  symggrp  18458  symgid  18459  lactghmga  18462  symgfixf1  18494  f1omvdmvd  18500  f1omvdconj  18503  f1omvdco2  18505  pmtrfconj  18523  symggen  18527  pmtrdifellem1  18533  pmtrdifellem2  18534  psgnunilem1  18550  gsumval3eu  18953  gsumval3lem1  18954  gsumval3  18956  gsumzf1o  18961  gsumconst  18983  gsumsub  18997  gsumcom2  19024  dprdfsub  19072  dprdf1o  19083  dprdsn  19087  ablfaclem2  19137  srngcl  19555  lmhmf1o  19747  fidomndrnglem  20007  psrass1lem  20085  psrnegcl  20104  psrlinv  20105  coe1f2  20305  coe1add  20360  evls1rhmlem  20412  evl1sca  20425  pf1ind  20446  gsumfsum  20540  zntoslem  20631  islinds2  20885  lindsmm  20900  mat1dimelbas  21008  mat1f  21019  mdetleib2  21125  mdetrsca  21140  mdetralt  21145  mdetunilem7  21155  mdetunilem9  21157  ssidcn  21791  hmphdis  22332  indishmph  22334  cmphaushmeo  22336  ordthmeolem  22337  txhmeo  22339  qtopf1  22352  ufldom  22498  symgtgp  22637  tsmsf1o  22680  iducn  22819  imasdsf1olem  22910  xpsdsval  22918  imasf1obl  23025  icchmeo  23472  iccpnfcnv  23475  xrhmeo  23477  cnheiborlem  23485  ovolctb  24018  ovoliunlem1  24030  ovoliunlem2  24031  iunmbl2  24085  dyadmbl  24128  vitalilem2  24137  vitalilem3  24138  vitalilem4  24139  vitalilem5  24140  mbfid  24163  dvid  24442  dvexp  24477  dvcnvlem  24500  dvcnv  24501  dvcnvrelem2  24542  dvcnvre  24543  efcvx  24964  reefgim  24965  efif1olem4  25056  eff1olem  25059  logrncl  25078  relogcl  25086  dvrelog  25147  relogcn  25148  logcn  25157  logf1o2  25160  dvlog  25161  dvlog2  25163  advlog  25164  advlogexp  25165  logtayl  25170  logccv  25173  dvcxp1  25248  loglesqrt  25266  asinrebnd  25406  dvatan  25440  efrlim  25474  amgmlem  25494  lgamcvg2  25559  wilthlem2  25573  wilthlem3  25574  sqff1o  25686  lgsqrlem4  25852  logdivsum  26036  log2sumbnd  26047  isismt  26247  motcl  26252  motco  26253  cnvmot  26254  motgrp  26256  motcgrg  26257  f1otrg  26584  f1otrge  26585  axlowdimlem10  26664  axcontlem5  26681  axcontlem10  26686  upgrres1  27022  umgrres1  27023  upgriseupth  27913  pliguhgr  28190  dmadjrn  29599  unopnorm  29621  unopadj  29623  unoplin  29624  counop  29625  idcnop  29685  idhmop  29686  unopbd  29719  bracnln  29813  cnvbraval  29814  leopnmid  29842  nmopleid  29843  hmopidmch  29857  hmopidmpj  29858  disjrdx  30269  fmptco1f1o  30306  isoun  30363  padct  30381  fcobij  30384  fcobijfs  30385  abliso  30610  symgfcoeu  30653  symgcom  30654  pmtrcnel  30660  pmtrcnel2  30661  pmtrcnelor  30662  cycpmco2f1  30693  cycpmco2rn  30694  cycpmco2lem2  30696  cycpmco2lem3  30697  cycpmco2lem4  30698  cycpmco2lem5  30699  cycpmco2lem6  30700  cycpmco2lem7  30701  cycpmco2  30702  cycpmconjv  30711  cycpmconjslem1  30723  cycpmconjslem2  30724  cycpmconjs  30725  islinds5  30859  ellspds  30860  tpr2rico  31054  xrge0iifmhm  31081  xrge0pluscn  31082  rrhre  31161  esumf1o  31208  volmeas  31389  eulerpartgbij  31529  eulerpartlemmf  31532  eulerpartlemgvv  31533  eulerpartlemgf  31536  eulerpartlemgs2  31537  eulerpartlemn  31538  ballotlemsima  31672  reprpmtf1o  31796  logdivsqrle  31820  hgt750lemg  31824  deranglem  32310  derangsn  32314  derangenlem  32315  subfacp1lem4  32327  subfacp1lem5  32328  subfacp1lem6  32329  cvmfolem  32423  cvmliftlem6  32434  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem4  34777  poimirlem6  34779  poimirlem7  34780  poimirlem9  34782  poimirlem11  34784  poimirlem12  34785  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem26  34799  poimirlem27  34800  poimirlem28  34801  poimirlem32  34805  mblfinlem2  34811  dvasin  34859  f1ocan1fv  34882  metf1o  34911  ismtyval  34959  isismty  34960  ismtyima  34962  ismtyhmeolem  34963  ismtybndlem  34965  ismrer1  34997  reheibor  34998  grposnOLD  35041  rngoisocnv  35140  lflnegl  36092  lautset  37098  islaut  37099  lautcl  37103  lautco  37113  pautsetN  37114  ispautN  37115  ldilco  37132  ltrncoidN  37144  ltrncoval  37161  trlcoabs2N  37738  trlcoat  37739  trlcone  37744  cdlemg47a  37750  cdlemg46  37751  cdlemg47  37752  trljco  37756  tgrpgrplem  37765  tendoidcl  37785  tendo0co2  37804  tendo0pl  37807  cdlemi2  37835  cdlemk2  37848  cdlemk4  37850  cdlemk8  37854  cdlemkid2  37940  cdlemk45  37963  cdlemk53b  37972  cdlemk53  37973  cdlemk55a  37975  erng1r  38011  tendocnv  38037  dvalveclem  38041  dva0g  38043  dvhgrp  38123  dvh0g  38127  dvhopN  38132  cdlemn3  38213  cdlemn8  38220  cdlemn9  38221  dihordlem7b  38231  dihopelvalcpre  38264  dihmeetlem1N  38306  dihglblem5apreN  38307  lcfrlem13  38571  hvmapclN  38780  hvmapcl2  38782  mapfzcons  39191  mzpresrename  39225  diophrw  39234  eldioph2  39237  diophren  39288  kelac1  39541  imasgim  39578  lnrfg  39597  brco2f1o  40260  brco3f1o  40261  clsneikex  40334  clsneinex  40335  clsneiel1  40336  neicvgmex  40345  neicvgel1  40347  dssmapntrcls  40356  stoweidlem27  42189  stoweidlem31  42193  stoweidlem39  42201  fourierdlem20  42289  fourierdlem50  42318  fourierdlem52  42320  fourierdlem54  42322  fourierdlem64  42332  fourierdlem76  42344  fourierdlem102  42370  fourierdlem114  42382  sge0f1o  42541  nnfoctbdjlem  42614  isomenndlem  42689  ovnsubaddlem1  42729  reuf1odnf  43183  reuf1od  43184  f1oresf1o2  43367  fundcmpsurbijinjpreimafv  43444  fundcmpsurinjimaid  43448  isomushgr  43868  isomuspgr  43876  isomgrtrlem  43880  1hegrlfgr  43884  mgmhmf1o  43931  idmgmhm  43932  ielefmnd  43984  symgsubmefmndALT  43996  funcringcsetcALTV2lem8  44242  funcringcsetclem8ALTV  44265  amgmwlem  44831
  Copyright terms: Public domain W3C validator