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

Theorem f1of 5629
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 5628 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5594 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   -->wf 5402   -1-1->wf1 5403   -1-1-onto->wf1o 5405
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 185  df-an 371  df-f1 5411  df-f1o 5413
This theorem is referenced by:  f1ofn  5630  f1ompt  5853  f1oresrab  5862  fsn  5868  fsnunf  5903  f1ocnvfv1  5970  f1ocnvfv2  5971  f1ocnvdm  5976  fcof1o  5984  fveqf1o  5987  isocnv  6008  isocnv3  6010  isores2  6011  isotr  6014  isofr2  6022  isopolem  6023  isosolem  6025  f1oiso2  6030  weniso  6032  f1ofveu  6074  f1oexrnex  6516  f1oabexg  6525  wemoiso  6551  suppsnop  6693  smoiso  6809  mapsn  7242  ralxpmap  7250  f1oen2g  7314  en1  7364  enfixsn  7408  mapen  7463  ac6sfi  7544  domunfican  7572  fiint  7576  mapfienlem1  7642  mapfienlem2  7643  mapfienlem3  7644  mapfien  7645  supisoex  7709  supiso  7710  ordiso2  7717  ordtypelem10  7729  hartogslem1  7744  unxpwdom2  7791  cantnfle  7867  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1d  7884  cantnflem1  7885  cantnfleOLD  7897  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1dOLD  7907  cantnflem1OLD  7908  mapfienOLD  7915  cnfcomlem  7920  cnfcom  7921  cnfcom2lem  7922  cnfcom2  7923  cnfcom3lem  7924  cnfcom3  7925  cnfcom3clem  7926  cnfcomlemOLD  7928  cnfcomOLD  7929  cnfcom2lemOLD  7930  cnfcom2OLD  7931  cnfcom3lemOLD  7932  cnfcom3OLD  7933  cnfcom3clemOLD  7934  infxpenlem  8168  infxpenc  8172  infxpenc2lem2  8174  infxpencOLD  8177  infxpenc2lem2OLD  8178  fseqenlem1  8182  acndom  8209  acndom2  8212  infpwfien  8220  iunfictbso  8272  infmap2  8375  ackbij2lem2  8397  infpssrlem3  8462  infpssrlem4  8463  fin23lem30  8499  isf32lem6  8515  isf32lem7  8516  isf32lem8  8517  enfin1ai  8541  axcc3  8595  axcclem  8614  ttukeylem7  8672  fpwwe2lem6  8790  fpwwe2lem7  8791  fpwwe2lem9  8793  canthp1lem2  8808  canthp1  8809  pwfseqlem4a  8816  pwfseqlem5  8818  dfle2  11112  axdc4uzlem  11788  seqf1olem1  11829  seqf1olem2  11830  seqf1o  11831  hashkf  12089  hasheqf1oi  12106  hashcl  12110  hashgadd  12124  hashfacen  12191  hashf1lem1  12192  fz1isolem  12198  seqcoll  12200  seqcoll2  12201  snopiswrd  12227  cnrecnv  12638  sumeq2ii  13154  summolem3  13175  summolem2a  13176  fsum  13181  fsumf1o  13184  fsumss  13186  fsumcl2lem  13192  fsumadd  13199  fsummulc2  13234  fsumrelem  13253  ackbijnn  13274  sadcaddlem  13636  sadadd2lem  13638  sadadd3  13640  sadaddlem  13645  sadasslem  13649  sadeq  13651  phimullem  13837  eulerthlem1  13839  eulerthlem2  13840  unbenlem  13952  vdwlem8  14032  0ram  14064  wunndx  14173  xpsaddlem  14496  xpsvsca  14500  xpsle  14502  idfucl  14774  setccatid  14935  setcinv  14941  catcisolem  14957  yonffthlem  15075  gsumws1  15497  idghm  15742  ghmf1o  15756  symgval  15864  symgbas  15865  elsymgbas  15867  symgbasf  15869  symgbasfi  15871  symg1bas  15881  symggrp  15885  symgid  15886  lactghmga  15889  symgfixf1  15923  f1omvdmvd  15929  f1omvdconj  15932  f1omvdco2  15934  pmtrfconj  15952  symggen  15956  pmtrdifellem1  15962  pmtrdifellem2  15963  psgnunilem1  15979  gsumval3eu  16361  gsumval3OLD  16362  gsumval3lem1  16363  gsumval3  16365  gsumzf1o  16371  gsumzf1oOLD  16374  gsumconst  16406  gsumsub  16423  gsumsubOLD  16424  gsumcom2  16441  dprdfsub  16485  dprdfsubOLD  16492  dprdf1o  16503  dprdsn  16507  ablfaclem2  16561  srngcl  16864  lmhmf1o  17049  fidomndrnglem  17300  psrass1lem  17381  psrnegcl  17401  psrlinv  17402  coe1f2  17564  coe1add  17616  gsumfsum  17723  zntoslem  17831  frgpcyg  17848  islinds2  18084  lindsmm  18099  mdetleib2  18241  mdetrsca  18252  mdetralt  18256  mdetunilem7  18266  mdetunilem9  18268  ssidcn  18701  hausdiag  19060  hmphdis  19211  indishmph  19213  cmphaushmeo  19215  ordthmeolem  19216  txhmeo  19218  pt1hmeo  19221  qtopf1  19231  ufldom  19377  symgtgp  19514  tsmsf1o  19561  iducn  19700  imasdsf1olem  19790  xpsdsval  19798  imasf1obl  19905  icchmeo  20355  iccpnfcnv  20358  xrhmeo  20360  cnheiborlem  20368  ovolctb  20815  ovoliunlem1  20827  ovoliunlem2  20828  iunmbl2  20880  dyadmbl  20922  vitalilem2  20931  vitalilem3  20932  vitalilem4  20933  vitalilem5  20934  mbfid  20956  dvid  21234  dvexp  21269  dvcnvlem  21290  dvcnv  21291  dvcnvrelem2  21332  dvcnvre  21333  evl1rhm  21380  evl1sca  21381  pf1ind  21406  efcvx  21799  reefgim  21800  efif1olem4  21886  eff1olem  21889  logrncl  21904  relogcl  21912  dvrelog  21967  relogcn  21968  logcn  21977  logf1o2  21980  dvlog  21981  dvlog2  21983  advlog  21984  advlogexp  21985  logtayl  21990  logccv  21993  dvcxp1  22065  loglesqr  22081  asinrebnd  22181  dvatan  22215  efrlim  22248  amgmlem  22268  wilthlem2  22292  wilthlem3  22293  sqff1o  22405  lgsqrlem4  22568  logdivsum  22667  log2sumbnd  22678  f1otrg  22940  f1otrge  22941  axlowdimlem10  23020  axcontlem5  23037  axcontlem10  23042  umgra1  23083  iseupa  23409  eupatrl  23412  eupa0  23418  eupares  23419  eupap1  23420  eupath2lem3  23423  grposn  23525  ginvsn  23659  dmadjrn  25122  unopnorm  25144  unopadj  25146  unoplin  25147  counop  25148  idcnop  25208  idhmop  25209  unopbd  25242  bracnln  25336  cnvbraval  25337  leopnmid  25365  nmopleid  25366  hmopidmch  25380  hmopidmpj  25381  disjrdx  25757  isoun  25821  fcobij  25849  fcobijfs  25850  abliso  25983  gsumpropd2lem  26093  tpr2rico  26196  xrge0iifmhm  26223  xrge0pluscn  26224  rrhre  26301  esumf1o  26358  volmeas  26501  eulerpartgbij  26603  eulerpartlemmf  26606  eulerpartlemgvv  26607  eulerpartlemgf  26610  eulerpartlemgs2  26611  eulerpartlemn  26612  ballotlemsima  26746  lgamcvg2  26889  deranglem  26902  derangsn  26906  derangenlem  26907  subfacp1lem4  26919  subfacp1lem5  26920  subfacp1lem6  26921  cvmfolem  27016  cvmliftlem6  27027  ghomsn  27154  prodeq2ii  27273  prodmolem3  27293  prodmolem2a  27294  fprod  27301  fprodf1o  27306  fprodss  27308  fprodser  27309  fprodcl2lem  27310  fprodmul  27318  fproddiv  27319  fprodn0  27337  mblfinlem2  28273  dvasin  28324  f1ocan1fv  28464  metf1o  28495  ismtyval  28543  isismty  28544  ismtyima  28546  ismtyhmeolem  28547  ismtybndlem  28549  ismrer1  28581  reheibor  28582  rngoisocnv  28631  mapfzcons  28897  mzpresrename  28932  diophrw  28942  eldioph2  28945  diophren  28997  kelac1  29261  imasgim  29300  lnrfg  29320  stoweidlem27  29668  stoweidlem31  29672  stoweidlem39  29680  lflnegl  32294  lautset  33299  islaut  33300  lautcl  33304  lautco  33314  pautsetN  33315  ispautN  33316  ldilco  33333  ltrncoidN  33345  ltrncoval  33362  trlcoabs2N  33939  trlcoat  33940  trlcone  33945  cdlemg47a  33951  cdlemg46  33952  cdlemg47  33953  trljco  33957  tgrpgrplem  33966  tendoidcl  33986  tendo0co2  34005  tendo0pl  34008  cdlemi2  34036  cdlemk2  34049  cdlemk4  34051  cdlemk8  34055  cdlemkid2  34141  cdlemk45  34164  cdlemk53b  34173  cdlemk53  34174  cdlemk55a  34176  erng1r  34212  tendocnv  34239  dvalveclem  34243  dva0g  34245  dvhgrp  34325  dvh0g  34329  dvhopN  34334  cdlemn3  34415  cdlemn8  34422  cdlemn9  34423  dihordlem7b  34433  dihopelvalcpre  34466  dihmeetlem1N  34508  dihglblem5apreN  34509  lcfrlem13  34773  hvmapclN  34982  hvmapcl2  34984
  Copyright terms: Public domain W3C validator