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

Theorem f1of 6104
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 6103 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 6068 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wf 5853  1-1wf1 5854  1-1-ontowf1o 5856
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 386  df-f1 5862  df-f1o 5864
This theorem is referenced by:  f1ofn  6105  f1ompt  6348  f1oresrab  6361  fsn  6367  fsnunf  6416  f1ocnvfv1  6497  f1ocnvfv2  6498  fsnex  6503  f1ocnvdm  6505  fcof1oinvd  6513  fveqf1o  6522  isocnv  6545  isocnv3  6547  isores2  6548  isotr  6551  isofr2  6559  isopolem  6560  isosolem  6562  f1oiso2  6567  weniso  6569  f1ofveu  6610  f1oexrnex  7077  f1oabexg  7087  wemoiso  7113  suppsnop  7269  smoiso  7419  mapsn  7859  ralxpmap  7867  f1oen2g  7932  en1  7983  enfixsn  8029  mapen  8084  ac6sfi  8164  domunfican  8193  fiint  8197  mapfienlem1  8270  mapfienlem2  8271  mapfienlem3  8272  mapfien  8273  supisoex  8340  supiso  8341  ordiso2  8380  ordtypelem10  8392  hartogslem1  8407  unxpwdom2  8453  cantnfle  8528  cantnfp1lem3  8537  cantnflem1b  8543  cantnflem1d  8545  cantnflem1  8546  cnfcomlem  8556  cnfcom  8557  cnfcom2lem  8558  cnfcom2  8559  cnfcom3lem  8560  cnfcom3  8561  cnfcom3clem  8562  infxpenlem  8796  infxpenc  8801  infxpenc2lem2  8803  fseqenlem1  8807  acndom  8834  acndom2  8837  infpwfien  8845  iunfictbso  8897  infmap2  9000  ackbij2lem2  9022  infpssrlem3  9087  infpssrlem4  9088  fin23lem30  9124  isf32lem6  9140  isf32lem7  9141  isf32lem8  9142  enfin1ai  9166  axcc3  9220  axcclem  9239  ttukeylem7  9297  fpwwe2lem6  9417  fpwwe2lem7  9418  fpwwe2lem9  9420  canthp1lem2  9435  canthp1  9436  pwfseqlem4a  9443  pwfseqlem5  9445  dfle2  11940  axdc4uzlem  12738  seqf1olem1  12796  seqf1olem2  12797  seqf1o  12798  hashkf  13075  hasheqf1oi  13096  hasheqf1oiOLD  13097  hasheqf1od  13100  hashcl  13103  hashgadd  13122  hashfacen  13192  hashf1lem1  13193  fz1isolem  13199  seqcoll  13202  seqcoll2  13203  cnrecnv  13855  sumeq2ii  14373  summolem3  14394  summolem2a  14395  fsum  14400  fsumf1o  14403  fsumss  14405  fsumcl2lem  14411  fsumadd  14419  fsummulc2  14463  fsumrelem  14485  ackbijnn  14504  prodeq2ii  14587  prodmolem3  14607  prodmolem2a  14608  fprod  14615  fprodf1o  14620  fprodss  14622  fprodser  14623  fprodcl2lem  14624  fprodmul  14634  fproddiv  14635  fprodn0  14653  fproddvdsd  15002  sadcaddlem  15122  sadadd2lem  15124  sadadd3  15126  sadaddlem  15131  sadasslem  15135  sadeq  15137  phimullem  15427  eulerthlem1  15429  eulerthlem2  15430  unbenlem  15555  vdwlem8  15635  0ram  15667  wunndx  15819  xpsaddlem  16175  xpsvsca  16179  xpsle  16181  idfucl  16481  setccatid  16674  setcinv  16680  catcisolem  16696  estrccatid  16712  funcestrcsetclem7  16726  funcestrcsetclem8  16727  funcsetcestrclem7  16741  funcsetcestrclem8  16742  yonffthlem  16862  gsumpropd2lem  17213  idmhm  17284  mhmf1o  17285  gsumws1  17316  idghm  17615  ghmf1o  17630  symgval  17739  symgbas  17740  elsymgbas  17742  symgbasf  17744  symgbasfi  17746  symg1bas  17756  symggrp  17760  symgid  17761  lactghmga  17764  symgfixf1  17797  f1omvdmvd  17803  f1omvdconj  17806  f1omvdco2  17808  pmtrfconj  17826  symggen  17830  pmtrdifellem1  17836  pmtrdifellem2  17837  psgnunilem1  17853  gsumval3eu  18245  gsumval3lem1  18246  gsumval3  18248  gsumzf1o  18253  gsumconst  18274  gsumsub  18288  gsumcom2  18314  dprdfsub  18360  dprdf1o  18371  dprdsn  18375  ablfaclem2  18425  srngcl  18795  lmhmf1o  18986  fidomndrnglem  19246  psrass1lem  19317  psrnegcl  19336  psrlinv  19337  coe1f2  19519  coe1add  19574  evls1rhmlem  19626  evl1sca  19638  pf1ind  19659  gsumfsum  19753  zntoslem  19845  islinds2  20092  lindsmm  20107  mat1dimelbas  20217  mat1f  20228  mdetleib2  20334  mdetrsca  20349  mdetralt  20354  mdetunilem7  20364  mdetunilem9  20366  ssidcn  20999  hausdiag  21388  hmphdis  21539  indishmph  21541  cmphaushmeo  21543  ordthmeolem  21544  txhmeo  21546  qtopf1  21559  ufldom  21706  symgtgp  21845  tsmsf1o  21888  iducn  22027  imasdsf1olem  22118  xpsdsval  22126  imasf1obl  22233  icchmeo  22680  iccpnfcnv  22683  xrhmeo  22685  cnheiborlem  22693  ovolctb  23198  ovoliunlem1  23210  ovoliunlem2  23211  iunmbl2  23265  dyadmbl  23308  vitalilem2  23318  vitalilem3  23319  vitalilem4  23320  vitalilem5  23321  mbfid  23343  dvid  23621  dvexp  23656  dvcnvlem  23677  dvcnv  23678  dvcnvrelem2  23719  dvcnvre  23720  efcvx  24141  reefgim  24142  efif1olem4  24229  eff1olem  24232  logrncl  24252  relogcl  24260  dvrelog  24317  relogcn  24318  logcn  24327  logf1o2  24330  dvlog  24331  dvlog2  24333  advlog  24334  advlogexp  24335  logtayl  24340  logccv  24343  dvcxp1  24415  loglesqrt  24433  asinrebnd  24562  dvatan  24596  efrlim  24630  amgmlem  24650  lgamcvg2  24715  wilthlem2  24729  wilthlem3  24730  sqff1o  24842  lgsqrlem4  25008  logdivsum  25156  log2sumbnd  25167  isismt  25363  motcl  25368  motco  25369  cnvmot  25370  motgrp  25372  motcgrg  25373  f1otrg  25685  f1otrge  25686  axlowdimlem10  25765  axcontlem5  25782  axcontlem10  25787  upgrres1  26127  umgrres1  26128  upgriseupth  26967  pliguhgr  27226  dmadjrn  28642  unopnorm  28664  unopadj  28666  unoplin  28667  counop  28668  idcnop  28728  idhmop  28729  unopbd  28762  bracnln  28856  cnvbraval  28857  leopnmid  28885  nmopleid  28886  hmopidmch  28900  hmopidmpj  28901  disjrdx  29290  isoun  29363  padct  29381  fcobij  29384  fcobijfs  29385  abliso  29523  symgfcoeu  29672  tpr2rico  29782  xrge0iifmhm  29809  xrge0pluscn  29810  rrhre  29889  esumf1o  29935  volmeas  30117  eulerpartgbij  30257  eulerpartlemmf  30260  eulerpartlemgvv  30261  eulerpartlemgf  30264  eulerpartlemgs2  30265  eulerpartlemn  30266  ballotlemsima  30400  deranglem  30909  derangsn  30913  derangenlem  30914  subfacp1lem4  30926  subfacp1lem5  30927  subfacp1lem6  30928  cvmfolem  31022  cvmliftlem6  31033  poimirlem1  33081  poimirlem2  33082  poimirlem3  33083  poimirlem4  33084  poimirlem6  33086  poimirlem7  33087  poimirlem9  33089  poimirlem11  33091  poimirlem12  33092  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem22  33102  poimirlem26  33106  poimirlem27  33107  poimirlem28  33108  poimirlem32  33112  mblfinlem2  33118  dvasin  33167  f1ocan1fv  33192  metf1o  33222  ismtyval  33270  isismty  33271  ismtyima  33273  ismtyhmeolem  33274  ismtybndlem  33276  ismrer1  33308  reheibor  33309  grposnOLD  33352  rngoisocnv  33451  lflnegl  33882  lautset  34887  islaut  34888  lautcl  34892  lautco  34902  pautsetN  34903  ispautN  34904  ldilco  34921  ltrncoidN  34933  ltrncoval  34950  trlcoabs2N  35529  trlcoat  35530  trlcone  35535  cdlemg47a  35541  cdlemg46  35542  cdlemg47  35543  trljco  35547  tgrpgrplem  35556  tendoidcl  35576  tendo0co2  35595  tendo0pl  35598  cdlemi2  35626  cdlemk2  35639  cdlemk4  35641  cdlemk8  35645  cdlemkid2  35731  cdlemk45  35754  cdlemk53b  35763  cdlemk53  35764  cdlemk55a  35766  erng1r  35802  tendocnv  35829  dvalveclem  35833  dva0g  35835  dvhgrp  35915  dvh0g  35919  dvhopN  35924  cdlemn3  36005  cdlemn8  36012  cdlemn9  36013  dihordlem7b  36023  dihopelvalcpre  36056  dihmeetlem1N  36098  dihglblem5apreN  36099  lcfrlem13  36363  hvmapclN  36572  hvmapcl2  36574  mapfzcons  36798  mzpresrename  36832  diophrw  36841  eldioph2  36844  diophren  36896  kelac1  37152  imasgim  37189  lnrfg  37209  brco2f1o  37851  brco3f1o  37852  clsneikex  37925  clsneinex  37926  clsneiel1  37927  neicvgmex  37936  neicvgel1  37938  dssmapntrcls  37947  mapsnd  38897  stoweidlem27  39581  stoweidlem31  39585  stoweidlem39  39593  fourierdlem20  39681  fourierdlem50  39710  fourierdlem52  39712  fourierdlem54  39714  fourierdlem64  39724  fourierdlem76  39736  fourierdlem102  39762  fourierdlem114  39774  sge0f1o  39936  nnfoctbdjlem  40009  isomenndlem  40081  ovnsubaddlem1  40121  1hegrlfgr  41031  mgmhmf1o  41105  idmgmhm  41106  funcringcsetcALTV2lem8  41361  funcringcsetclem8ALTV  41384  amgmwlem  41881
  Copyright terms: Public domain W3C validator