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

Theorem f1of 5831
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 5830 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5796 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
31, 2syl 17 1  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   -->wf 5597   -1-1->wf1 5598   -1-1-onto->wf1o 5600
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 188  df-an 372  df-f1 5606  df-f1o 5608
This theorem is referenced by:  f1ofn  5832  f1ompt  6059  f1oresrab  6070  fsn  6076  fsnunf  6117  f1ocnvfv1  6190  f1ocnvfv2  6191  fsnex  6196  f1ocnvdm  6198  fcof1oinvd  6206  fveqf1o  6215  isocnv  6236  isocnv3  6238  isores2  6239  isotr  6242  isofr2  6250  isopolem  6251  isosolem  6253  f1oiso2  6258  weniso  6260  f1ofveu  6300  f1oexrnex  6756  f1oabexg  6766  wemoiso  6792  suppsnop  6939  smoiso  7092  mapsn  7524  ralxpmap  7532  f1oen2g  7596  en1  7646  enfixsn  7690  mapen  7745  ac6sfi  7824  domunfican  7853  fiint  7857  mapfienlem1  7927  mapfienlem2  7928  mapfienlem3  7929  mapfien  7930  supisoex  7999  supiso  8000  ordiso2  8039  ordtypelem10  8051  hartogslem1  8066  unxpwdom2  8112  cantnfle  8184  cantnfp1lem3  8193  cantnflem1b  8199  cantnflem1d  8201  cantnflem1  8202  cnfcomlem  8212  cnfcom  8213  cnfcom2lem  8214  cnfcom2  8215  cnfcom3lem  8216  cnfcom3  8217  cnfcom3clem  8218  infxpenlem  8452  infxpenc  8456  infxpenc2lem2  8458  fseqenlem1  8462  acndom  8489  acndom2  8492  infpwfien  8500  iunfictbso  8552  infmap2  8655  ackbij2lem2  8677  infpssrlem3  8742  infpssrlem4  8743  fin23lem30  8779  isf32lem6  8795  isf32lem7  8796  isf32lem8  8797  enfin1ai  8821  axcc3  8875  axcclem  8894  ttukeylem7  8952  fpwwe2lem6  9067  fpwwe2lem7  9068  fpwwe2lem9  9070  canthp1lem2  9085  canthp1  9086  pwfseqlem4a  9093  pwfseqlem5  9095  dfle2  11453  axdc4uzlem  12201  seqf1olem1  12258  seqf1olem2  12259  seqf1o  12260  hashkf  12523  hasheqf1oi  12540  hashcl  12544  hashgadd  12562  hashfacen  12621  hashf1lem1  12622  fz1isolem  12628  seqcoll  12631  seqcoll2  12632  snopiswrd  12685  cnrecnv  13228  sumeq2ii  13758  summolem3  13779  summolem2a  13780  fsum  13785  fsumf1o  13788  fsumss  13790  fsumcl2lem  13796  fsumadd  13804  fsummulc2  13844  fsumrelem  13866  ackbijnn  13885  prodeq2ii  13966  prodmolem3  13986  prodmolem2a  13987  fprod  13994  fprodf1o  13999  fprodss  14001  fprodser  14002  fprodcl2lem  14003  fprodmul  14013  fproddiv  14014  fprodn0  14032  sadcaddlem  14430  sadadd2lem  14432  sadadd3  14434  sadaddlem  14439  sadasslem  14443  sadeq  14445  phimullem  14726  eulerthlem1  14728  eulerthlem2  14729  unbenlem  14851  vdwlem8  14937  0ram  14977  wunndx  15136  xpsaddlem  15480  xpsvsca  15484  xpsle  15486  idfucl  15785  setccatid  15978  setcinv  15984  catcisolem  16000  estrccatid  16016  funcestrcsetclem7  16030  funcestrcsetclem8  16031  funcsetcestrclem7  16045  funcsetcestrclem8  16046  yonffthlem  16166  gsumpropd2lem  16515  idmhm  16590  mhmf1o  16591  gsumws1  16622  idghm  16897  ghmf1o  16911  symgval  17019  symgbas  17020  elsymgbas  17022  symgbasf  17024  symgbasfi  17026  symg1bas  17036  symggrp  17040  symgid  17041  lactghmga  17044  symgfixf1  17077  f1omvdmvd  17083  f1omvdconj  17086  f1omvdco2  17088  pmtrfconj  17106  symggen  17110  pmtrdifellem1  17116  pmtrdifellem2  17117  psgnunilem1  17133  gsumval3eu  17537  gsumval3lem1  17538  gsumval3  17540  gsumzf1o  17545  gsumconst  17566  gsumsub  17580  gsumcom2  17606  dprdfsub  17653  dprdf1o  17664  dprdsn  17668  ablfaclem2  17718  srngcl  18082  lmhmf1o  18268  fidomndrnglem  18529  psrass1lem  18600  psrnegcl  18619  psrlinv  18620  coe1f2  18801  coe1add  18856  evls1rhmlem  18909  evl1sca  18921  pf1ind  18942  gsumfsum  19033  zntoslem  19125  frgpcyg  19142  islinds2  19369  lindsmm  19384  mat1dimelbas  19494  mat1dimmul  19499  mat1f  19505  mdetleib2  19611  mdetrsca  19626  mdetralt  19631  mdetunilem7  19641  mdetunilem9  19643  ssidcn  20269  hausdiag  20658  hmphdis  20809  indishmph  20811  cmphaushmeo  20813  ordthmeolem  20814  txhmeo  20816  pt1hmeo  20819  qtopf1  20829  ufldom  20975  symgtgp  21114  tsmsf1o  21157  iducn  21296  imasdsf1olem  21386  xpsdsval  21394  imasf1obl  21501  icchmeo  21967  iccpnfcnv  21970  xrhmeo  21972  cnheiborlem  21980  ovolctb  22441  ovoliunlem1  22453  ovoliunlem2  22454  iunmbl2  22508  dyadmbl  22556  vitalilem2  22565  vitalilem3  22566  vitalilem4  22567  vitalilem5  22568  mbfid  22590  dvid  22870  dvexp  22905  dvcnvlem  22926  dvcnv  22927  dvcnvrelem2  22968  dvcnvre  22969  efcvx  23402  reefgim  23403  efif1olem4  23492  eff1olem  23495  logrncl  23515  relogcl  23523  dvrelog  23580  relogcn  23581  logcn  23590  logf1o2  23593  dvlog  23594  dvlog2  23596  advlog  23597  advlogexp  23598  logtayl  23603  logccv  23606  dvcxp1  23678  loglesqrt  23696  asinrebnd  23825  dvatan  23859  efrlim  23893  amgmlem  23913  lgamcvg2  23978  wilthlem2  23992  wilthlem3  23993  sqff1o  24107  lgsqrlem4  24270  logdivsum  24369  log2sumbnd  24380  isismt  24577  motcl  24582  motco  24583  cnvmot  24584  motgrp  24586  motcgrg  24587  f1otrg  24899  f1otrge  24900  axlowdimlem10  24979  axcontlem5  24996  axcontlem10  25001  umgra1  25051  iseupa  25691  eupatrl  25694  eupa0  25700  eupares  25701  eupap1  25702  eupath2lem3  25705  grposn  25941  ginvsn  26075  dmadjrn  27546  unopnorm  27568  unopadj  27570  unoplin  27571  counop  27572  idcnop  27632  idhmop  27633  unopbd  27666  bracnln  27760  cnvbraval  27761  leopnmid  27789  nmopleid  27790  hmopidmch  27804  hmopidmpj  27805  disjrdx  28203  isoun  28284  padct  28313  fcobij  28316  fcobijfs  28317  abliso  28466  symgfcoeu  28616  tpr2rico  28726  xrge0iifmhm  28753  xrge0pluscn  28754  rrhre  28833  esumf1o  28879  volmeas  29062  eulerpartgbij  29213  eulerpartlemmf  29216  eulerpartlemgvv  29217  eulerpartlemgf  29220  eulerpartlemgs2  29221  eulerpartlemn  29222  ballotlemsima  29356  ballotlemsimaOLD  29394  deranglem  29897  derangsn  29901  derangenlem  29902  subfacp1lem4  29914  subfacp1lem5  29915  subfacp1lem6  29916  cvmfolem  30010  cvmliftlem6  30021  ghomsn  30314  poimirlem1  31905  poimirlem2  31906  poimirlem3  31907  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem9  31913  poimirlem11  31915  poimirlem12  31916  poimirlem16  31920  poimirlem17  31921  poimirlem19  31923  poimirlem20  31924  poimirlem22  31926  poimirlem26  31930  poimirlem27  31931  poimirlem28  31932  poimirlem32  31936  mblfinlem2  31942  dvasin  31992  f1ocan1fv  32017  metf1o  32048  ismtyval  32096  isismty  32097  ismtyima  32099  ismtyhmeolem  32100  ismtybndlem  32102  ismrer1  32134  reheibor  32135  rngoisocnv  32184  lflnegl  32611  lautset  33616  islaut  33617  lautcl  33621  lautco  33631  pautsetN  33632  ispautN  33633  ldilco  33650  ltrncoidN  33662  ltrncoval  33679  trlcoabs2N  34258  trlcoat  34259  trlcone  34264  cdlemg47a  34270  cdlemg46  34271  cdlemg47  34272  trljco  34276  tgrpgrplem  34285  tendoidcl  34305  tendo0co2  34324  tendo0pl  34327  cdlemi2  34355  cdlemk2  34368  cdlemk4  34370  cdlemk8  34374  cdlemkid2  34460  cdlemk45  34483  cdlemk53b  34492  cdlemk53  34493  cdlemk55a  34495  erng1r  34531  tendocnv  34558  dvalveclem  34562  dva0g  34564  dvhgrp  34644  dvh0g  34648  dvhopN  34653  cdlemn3  34734  cdlemn8  34741  cdlemn9  34742  dihordlem7b  34752  dihopelvalcpre  34785  dihmeetlem1N  34827  dihglblem5apreN  34828  lcfrlem13  35092  hvmapclN  35301  hvmapcl2  35303  mapfzcons  35527  mzpresrename  35561  diophrw  35570  eldioph2  35573  diophren  35625  kelac1  35891  imasgim  35928  lnrfg  35948  stoweidlem27  37827  stoweidlem31  37832  stoweidlem39  37840  fourierdlem20  37929  fourierdlem50  37960  fourierdlem52  37962  fourierdlem54  37964  fourierdlem64  37974  fourierdlem76  37986  fourierdlem102  38012  fourierdlem114  38024  sge0f1o  38132  nnfoctbdjlem  38201  isomenndlem  38259  ovnsubaddlem1  38296  nnsum3primesprm  38755  umgr1  39015  umgrres1  39149  mgmhmf1o  39407  idmgmhm  39408  funcringcsetcALTV2lem8  39665  funcringcsetclem8ALTV  39688
  Copyright terms: Public domain W3C validator