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

Theorem f1of 6784
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 6783 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 6738 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wf 6492  1-1wf1 6493  1-1-ontowf1o 6495
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 206  df-an 397  df-f1 6501  df-f1o 6503
This theorem is referenced by:  f1ofn  6785  f1ompt  7058  f1oresrab  7072  fsn  7080  fsnunf  7130  f1ocnvfv1  7221  f1ocnvfv2  7222  fsnex  7228  f1ocnvdm  7230  fcof1oinvd  7238  fveqf1o  7248  isocnv  7274  isocnv3  7276  isores2  7277  isotr  7280  isofr2  7288  isopolem  7289  isosolem  7291  f1oiso2  7296  weniso  7298  f1ofveu  7350  f1oexrnex  7863  f1oabexg  7872  wemoiso  7905  suppsnop  8108  smoiso  8307  mapsnd  8823  ralxpmap  8833  f1oen2g  8907  en1  8964  en1OLD  8965  enfixsn  9024  mapen  9084  ac6sfi  9230  domunfican  9263  fiint  9267  mapfienlem1  9340  mapfienlem2  9341  mapfienlem3  9342  mapfien  9343  supisoex  9409  supiso  9410  ordiso2  9450  unxpwdom2  9523  cantnfle  9606  cantnfp1lem3  9615  cantnflem1b  9621  cantnflem1d  9623  cantnflem1  9624  cnfcomlem  9634  cnfcom  9635  cnfcom2lem  9636  cnfcom2  9637  cnfcom3lem  9638  cnfcom3  9639  cnfcom3clem  9640  djuin  9853  infxpenlem  9948  infxpenc  9953  infxpenc2lem2  9955  fseqenlem1  9959  acndom  9986  acndom2  9989  infpwfien  9997  iunfictbso  10049  infmap2  10153  ackbij2lem2  10175  infpssrlem3  10240  infpssrlem4  10241  fin23lem30  10277  isf32lem6  10293  isf32lem7  10294  isf32lem8  10295  enfin1ai  10319  axcc3  10373  axcclem  10392  ttukeylem7  10450  fpwwe2lem5  10570  fpwwe2lem6  10571  fpwwe2lem8  10573  canthp1lem2  10588  canthp1  10589  pwfseqlem4a  10596  pwfseqlem5  10598  axdc4uzlem  13887  seqf1olem1  13946  seqf1olem2  13947  seqf1o  13948  hashkf  14231  hasheqf1oi  14250  hasheqf1od  14252  hashcl  14255  hashgadd  14276  hashfacen  14350  hashfacenOLD  14351  hashf1lem1  14352  hashf1lem1OLD  14353  fz1isolem  14359  seqcoll  14362  seqcoll2  14363  cnrecnv  15049  sumeq2ii  15577  summolem3  15598  summolem2a  15599  fsum  15604  fsumf1o  15607  fsumss  15609  fsumcl2lem  15615  fsumadd  15624  fsummulc2  15668  fsumrelem  15691  ackbijnn  15712  prodeq2ii  15795  prodmolem3  15815  prodmolem2a  15816  fprod  15823  fprodf1o  15828  fprodss  15830  fprodser  15831  fprodcl2lem  15832  fprodmul  15842  fproddiv  15843  fprodn0  15861  fproddvdsd  16216  sadcaddlem  16336  sadadd2lem  16338  sadadd3  16340  sadaddlem  16345  sadasslem  16349  sadeq  16351  phimullem  16650  eulerthlem1  16652  eulerthlem2  16653  unbenlem  16779  vdwlem8  16859  0ram  16891  wunndx  17066  xpsaddlem  17454  xpsvsca  17458  xpsle  17460  idfucl  17766  setccatid  17969  setcinv  17975  catcisolem  17995  estrccatid  18018  funcestrcsetclem7  18033  funcestrcsetclem8  18034  funcsetcestrclem7  18048  funcsetcestrclem8  18049  yonffthlem  18170  gsumpropd2lem  18533  idmhm  18610  mhmf1o  18611  gsumws1  18647  ielefmnd  18696  idghm  19021  ghmf1o  19036  permsetexOLD  19149  symgbas  19150  elsymgbas  19153  symgbasf  19155  symgbasfi  19158  symg1bas  19170  symggrp  19180  lactghmga  19185  symgfixf1  19217  f1omvdmvd  19223  f1omvdconj  19226  f1omvdco2  19228  pmtrfconj  19246  symggen  19250  pmtrdifellem1  19256  pmtrdifellem2  19257  psgnunilem1  19273  gsumval3eu  19679  gsumval3lem1  19680  gsumval3  19682  gsumzf1o  19687  gsumconst  19709  gsumsub  19723  gsumcom2  19750  dprdfsub  19798  dprdf1o  19809  dprdsn  19813  ablfaclem2  19863  srngcl  20312  lmhmf1o  20505  fidomndrnglem  20775  gsumfsum  20862  zntoslem  20961  islinds2  21217  lindsmm  21232  psrass1lemOLD  21340  psrass1lem  21343  psrnegcl  21362  psrlinv  21363  coe1f2  21578  coe1add  21633  evls1rhmlem  21685  evl1sca  21698  pf1ind  21719  mat1dimelbas  21818  mat1f  21829  mdetleib2  21935  mdetrsca  21950  mdetralt  21955  mdetunilem7  21965  mdetunilem9  21967  ssidcn  22604  hmphdis  23145  indishmph  23147  cmphaushmeo  23149  ordthmeolem  23150  txhmeo  23152  qtopf1  23165  ufldom  23311  symgtgp  23455  tsmsf1o  23494  iducn  23633  imasdsf1olem  23724  xpsdsval  23732  imasf1obl  23842  icchmeo  24302  iccpnfcnv  24305  xrhmeo  24307  cnheiborlem  24315  ovolctb  24852  ovoliunlem1  24864  ovoliunlem2  24865  iunmbl2  24919  dyadmbl  24962  vitalilem2  24971  vitalilem3  24972  vitalilem4  24973  vitalilem5  24974  mbfid  24997  dvid  25280  dvexp  25315  dvcnvlem  25338  dvcnv  25339  dvcnvrelem2  25380  dvcnvre  25381  efcvx  25806  reefgim  25807  efif1olem4  25899  eff1olem  25902  logrncl  25921  relogcl  25929  dvrelog  25990  relogcn  25991  logcn  26000  logf1o2  26003  dvlog  26004  dvlog2  26006  advlog  26007  advlogexp  26008  logtayl  26013  logccv  26016  dvcxp1  26091  loglesqrt  26109  asinrebnd  26249  dvatan  26283  efrlim  26317  amgmlem  26337  lgamcvg2  26402  wilthlem2  26416  wilthlem3  26417  sqff1o  26529  lgsqrlem4  26695  logdivsum  26879  log2sumbnd  26890  isismt  27423  motcl  27428  motco  27429  cnvmot  27430  motgrp  27432  motcgrg  27433  f1otrg  27760  f1otrge  27761  axlowdimlem10  27847  axcontlem5  27864  axcontlem10  27869  upgrres1  28208  umgrres1  28209  upgriseupth  29098  pliguhgr  29375  dmadjrn  30784  unopnorm  30806  unopadj  30808  unoplin  30809  counop  30810  idcnop  30870  idhmop  30871  unopbd  30904  bracnln  30998  cnvbraval  30999  leopnmid  31027  nmopleid  31028  hmopidmch  31042  hmopidmpj  31043  disjrdx  31456  fmptco1f1o  31494  isoun  31560  padct  31580  fcobij  31583  fcobijfs  31584  abliso  31831  symgfcoeu  31877  symgcom  31878  pmtrcnel  31884  pmtrcnel2  31885  pmtrcnelor  31886  cycpmco2f1  31917  cycpmco2rn  31918  cycpmco2lem2  31920  cycpmco2lem3  31921  cycpmco2lem4  31922  cycpmco2lem5  31923  cycpmco2lem6  31924  cycpmco2lem7  31925  cycpmco2  31926  cycpmconjv  31935  cycpmconjslem1  31947  cycpmconjslem2  31948  cycpmconjs  31949  islinds5  32100  ellspds  32101  tpr2rico  32433  xrge0iifmhm  32460  xrge0pluscn  32461  rrhre  32542  esumf1o  32589  volmeas  32770  eulerpartgbij  32912  eulerpartlemmf  32915  eulerpartlemgvv  32916  eulerpartlemgf  32919  eulerpartlemgs2  32920  eulerpartlemn  32921  ballotlemsima  33055  reprpmtf1o  33179  logdivsqrle  33203  hgt750lemg  33207  deranglem  33700  derangsn  33704  derangenlem  33705  subfacp1lem4  33717  subfacp1lem5  33718  subfacp1lem6  33719  cvmfolem  33813  cvmliftlem6  33824  poimirlem1  36069  poimirlem2  36070  poimirlem3  36071  poimirlem4  36072  poimirlem6  36074  poimirlem7  36075  poimirlem9  36077  poimirlem11  36079  poimirlem12  36080  poimirlem16  36084  poimirlem17  36085  poimirlem19  36087  poimirlem20  36088  poimirlem22  36090  poimirlem26  36094  poimirlem27  36095  poimirlem28  36096  poimirlem32  36100  mblfinlem2  36106  dvasin  36152  f1ocan1fv  36175  metf1o  36204  ismtyval  36249  isismty  36250  ismtyima  36252  ismtyhmeolem  36253  ismtybndlem  36255  ismrer1  36287  reheibor  36288  grposnOLD  36331  rngoisocnv  36430  lflnegl  37528  lautset  38535  islaut  38536  lautcl  38540  lautco  38550  pautsetN  38551  ispautN  38552  ldilco  38569  ltrncoidN  38581  ltrncoval  38598  trlcoabs2N  39175  trlcoat  39176  trlcone  39181  cdlemg47a  39187  cdlemg46  39188  cdlemg47  39189  trljco  39193  tgrpgrplem  39202  tendoidcl  39222  tendo0co2  39241  tendo0pl  39244  cdlemi2  39272  cdlemk2  39285  cdlemk4  39287  cdlemk8  39291  cdlemkid2  39377  cdlemk45  39400  cdlemk53b  39409  cdlemk53  39410  cdlemk55a  39412  erng1r  39448  tendocnv  39474  dvalveclem  39478  dva0g  39480  dvhgrp  39560  dvh0g  39564  dvhopN  39569  cdlemn3  39650  cdlemn8  39657  cdlemn9  39658  dihordlem7b  39668  dihopelvalcpre  39701  dihmeetlem1N  39743  dihglblem5apreN  39744  lcfrlem13  40008  hvmapclN  40217  hvmapcl2  40219  dvrelog2  40511  dvrelog3  40512  sticksstones3  40546  sticksstones17  40561  sticksstones18  40562  sticksstones19  40563  metakunt33  40599  mapfzcons  41016  mzpresrename  41050  diophrw  41059  eldioph2  41062  diophren  41113  kelac1  41367  imasgim  41404  lnrfg  41423  nvocnvb  41675  brco2f1o  42285  brco3f1o  42286  clsneikex  42359  clsneinex  42360  clsneiel1  42361  neicvgmex  42370  neicvgel1  42372  dssmapntrcls  42381  stoweidlem27  44239  stoweidlem31  44243  stoweidlem39  44251  fourierdlem20  44339  fourierdlem50  44368  fourierdlem52  44370  fourierdlem54  44372  fourierdlem64  44382  fourierdlem76  44394  fourierdlem102  44420  fourierdlem114  44432  sge0f1o  44594  nnfoctbdjlem  44667  isomenndlem  44742  ovnsubaddlem1  44782  reuf1odnf  45310  reuf1od  45311  f1oresf1o2  45494  fundcmpsurbijinjpreimafv  45570  fundcmpsurinjimaid  45574  isomushgr  45989  isomuspgr  45997  isomgrtrlem  46001  1hegrlfgr  46005  mgmhmf1o  46052  idmgmhm  46053  funcringcsetcALTV2lem8  46312  funcringcsetclem8ALTV  46335  itcovalendof  46726  thincciso  47040  amgmwlem  47220
  Copyright terms: Public domain W3C validator