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

Theorem f1of 5802
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 5801 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5767 . 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 5570   -1-1->wf1 5571   -1-1-onto->wf1o 5573
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 5579  df-f1o 5581
This theorem is referenced by:  f1ofn  5803  f1ompt  6034  f1oresrab  6044  fsn  6050  fsnunf  6090  f1ocnvfv1  6163  f1ocnvfv2  6164  f1ocnvdm  6169  fcof1oinvd  6177  fveqf1o  6186  isocnv  6207  isocnv3  6209  isores2  6210  isotr  6213  isofr2  6221  isopolem  6222  isosolem  6224  f1oiso2  6229  weniso  6231  f1ofveu  6272  f1oexrnex  6730  f1oabexg  6740  wemoiso  6766  suppsnop  6913  smoiso  7031  mapsn  7458  ralxpmap  7466  f1oen2g  7530  en1  7580  enfixsn  7624  mapen  7679  ac6sfi  7762  domunfican  7791  fiint  7795  mapfienlem1  7862  mapfienlem2  7863  mapfienlem3  7864  mapfien  7865  supisoex  7930  supiso  7931  ordiso2  7938  ordtypelem10  7950  hartogslem1  7965  unxpwdom2  8012  cantnfle  8088  cantnfp1lem3  8097  cantnflem1b  8103  cantnflem1d  8105  cantnflem1  8106  cantnfleOLD  8118  cantnfp1lem3OLD  8123  cantnflem1bOLD  8126  cantnflem1dOLD  8128  cantnflem1OLD  8129  mapfienOLD  8136  cnfcomlem  8141  cnfcom  8142  cnfcom2lem  8143  cnfcom2  8144  cnfcom3lem  8145  cnfcom3  8146  cnfcom3clem  8147  cnfcomlemOLD  8149  cnfcomOLD  8150  cnfcom2lemOLD  8151  cnfcom2OLD  8152  cnfcom3lemOLD  8153  cnfcom3OLD  8154  cnfcom3clemOLD  8155  infxpenlem  8389  infxpenc  8393  infxpenc2lem2  8395  infxpencOLD  8398  infxpenc2lem2OLD  8399  fseqenlem1  8403  acndom  8430  acndom2  8433  infpwfien  8441  iunfictbso  8493  infmap2  8596  ackbij2lem2  8618  infpssrlem3  8683  infpssrlem4  8684  fin23lem30  8720  isf32lem6  8736  isf32lem7  8737  isf32lem8  8738  enfin1ai  8762  axcc3  8816  axcclem  8835  ttukeylem7  8893  fpwwe2lem6  9011  fpwwe2lem7  9012  fpwwe2lem9  9014  canthp1lem2  9029  canthp1  9030  pwfseqlem4a  9037  pwfseqlem5  9039  dfle2  11357  axdc4uzlem  12066  seqf1olem1  12120  seqf1olem2  12121  seqf1o  12122  hashkf  12381  hasheqf1oi  12398  hashcl  12402  hashgadd  12419  hashfacen  12477  hashf1lem1  12478  fz1isolem  12484  seqcoll  12486  seqcoll2  12487  snopiswrd  12530  cnrecnv  12972  sumeq2ii  13489  summolem3  13510  summolem2a  13511  fsum  13516  fsumf1o  13519  fsumss  13521  fsumcl2lem  13527  fsumadd  13535  fsummulc2  13573  fsumrelem  13595  ackbijnn  13614  sadcaddlem  13979  sadadd2lem  13981  sadadd3  13983  sadaddlem  13988  sadasslem  13992  sadeq  13994  phimullem  14181  eulerthlem1  14183  eulerthlem2  14184  unbenlem  14298  vdwlem8  14378  0ram  14410  wunndx  14520  xpsaddlem  14844  xpsvsca  14848  xpsle  14850  idfucl  15119  setccatid  15280  setcinv  15286  catcisolem  15302  yonffthlem  15420  gsumpropd2lem  15769  idmhm  15844  mhmf1o  15845  gsumws1  15876  idghm  16151  ghmf1o  16165  symgval  16273  symgbas  16274  elsymgbas  16276  symgbasf  16278  symgbasfi  16280  symg1bas  16290  symggrp  16294  symgid  16295  lactghmga  16298  symgfixf1  16331  f1omvdmvd  16337  f1omvdconj  16340  f1omvdco2  16342  pmtrfconj  16360  symggen  16364  pmtrdifellem1  16370  pmtrdifellem2  16371  psgnunilem1  16387  gsumval3eu  16776  gsumval3OLD  16777  gsumval3lem1  16778  gsumval3  16780  gsumzf1o  16786  gsumzf1oOLD  16789  gsumconst  16823  gsumsub  16843  gsumsubOLD  16844  gsumcom2  16872  dprdfsub  16929  dprdfsubOLD  16936  dprdf1o  16947  dprdsn  16951  ablfaclem2  17005  srngcl  17372  lmhmf1o  17560  fidomndrnglem  17823  psrass1lem  17897  psrnegcl  17917  psrlinv  17918  coe1f2  18116  coe1add  18173  evls1rhmlem  18226  evl1sca  18238  pf1ind  18259  gsumfsum  18352  zntoslem  18462  frgpcyg  18479  islinds2  18715  lindsmm  18730  mat1dimelbas  18840  mat1dimmul  18845  mat1f  18851  mdetleib2  18957  mdetrsca  18972  mdetralt  18977  mdetunilem7  18987  mdetunilem9  18989  ssidcn  19622  hausdiag  20012  hmphdis  20163  indishmph  20165  cmphaushmeo  20167  ordthmeolem  20168  txhmeo  20170  pt1hmeo  20173  qtopf1  20183  ufldom  20329  symgtgp  20466  tsmsf1o  20513  iducn  20652  imasdsf1olem  20742  xpsdsval  20750  imasf1obl  20857  icchmeo  21307  iccpnfcnv  21310  xrhmeo  21312  cnheiborlem  21320  ovolctb  21767  ovoliunlem1  21779  ovoliunlem2  21780  iunmbl2  21833  dyadmbl  21875  vitalilem2  21884  vitalilem3  21885  vitalilem4  21886  vitalilem5  21887  mbfid  21909  dvid  22187  dvexp  22222  dvcnvlem  22243  dvcnv  22244  dvcnvrelem2  22285  dvcnvre  22286  efcvx  22709  reefgim  22710  efif1olem4  22797  eff1olem  22800  logrncl  22820  relogcl  22828  dvrelog  22883  relogcn  22884  logcn  22893  logf1o2  22896  dvlog  22897  dvlog2  22899  advlog  22900  advlogexp  22901  logtayl  22906  logccv  22909  dvcxp1  22981  loglesqrt  22997  asinrebnd  23097  dvatan  23131  efrlim  23164  amgmlem  23184  wilthlem2  23208  wilthlem3  23209  sqff1o  23321  lgsqrlem4  23484  logdivsum  23583  log2sumbnd  23594  isismt  23786  motcl  23791  motco  23792  cnvmot  23793  motgrp  23795  motcgrg  23796  f1otrg  24039  f1otrge  24040  axlowdimlem10  24119  axcontlem5  24136  axcontlem10  24141  umgra1  24191  iseupa  24830  eupatrl  24833  eupa0  24839  eupares  24840  eupap1  24841  eupath2lem3  24844  grposn  25082  ginvsn  25216  dmadjrn  26679  unopnorm  26701  unopadj  26703  unoplin  26704  counop  26705  idcnop  26765  idhmop  26766  unopbd  26799  bracnln  26893  cnvbraval  26894  leopnmid  26922  nmopleid  26923  hmopidmch  26937  hmopidmpj  26938  disjrdx  27315  isoun  27385  fcobij  27413  fcobijfs  27414  abliso  27552  tpr2rico  27760  xrge0iifmhm  27787  xrge0pluscn  27788  rrhre  27865  esumf1o  27927  volmeas  28069  eulerpartgbij  28177  eulerpartlemmf  28180  eulerpartlemgvv  28181  eulerpartlemgf  28184  eulerpartlemgs2  28185  eulerpartlemn  28186  ballotlemsima  28320  lgamcvg2  28463  deranglem  28476  derangsn  28480  derangenlem  28481  subfacp1lem4  28493  subfacp1lem5  28494  subfacp1lem6  28495  cvmfolem  28590  cvmliftlem6  28601  ghomsn  28894  prodeq2ii  29013  prodmolem3  29033  prodmolem2a  29034  fprod  29041  fprodf1o  29046  fprodss  29048  fprodser  29049  fprodcl2lem  29050  fprodmul  29058  fproddiv  29059  fprodn0  29077  mblfinlem2  30020  dvasin  30071  f1ocan1fv  30185  metf1o  30216  ismtyval  30264  isismty  30265  ismtyima  30267  ismtyhmeolem  30268  ismtybndlem  30270  ismrer1  30302  reheibor  30303  rngoisocnv  30352  mapfzcons  30616  mzpresrename  30651  diophrw  30660  eldioph2  30663  diophren  30715  kelac1  30977  imasgim  31016  lnrfg  31036  stoweidlem27  31694  stoweidlem31  31698  stoweidlem39  31706  fourierdlem20  31794  fourierdlem50  31824  fourierdlem52  31826  fourierdlem54  31828  fourierdlem64  31838  fourierdlem76  31850  fourierdlem102  31876  fourierdlem114  31888  mgmhmf1o  32309  idmgmhm  32310  estrccatid  32476  funcringcsetclem8  32563  funcringcsetclem8OLD  32586  lflnegl  34503  lautset  35508  islaut  35509  lautcl  35513  lautco  35523  pautsetN  35524  ispautN  35525  ldilco  35542  ltrncoidN  35554  ltrncoval  35571  trlcoabs2N  36150  trlcoat  36151  trlcone  36156  cdlemg47a  36162  cdlemg46  36163  cdlemg47  36164  trljco  36168  tgrpgrplem  36177  tendoidcl  36197  tendo0co2  36216  tendo0pl  36219  cdlemi2  36247  cdlemk2  36260  cdlemk4  36262  cdlemk8  36266  cdlemkid2  36352  cdlemk45  36375  cdlemk53b  36384  cdlemk53  36385  cdlemk55a  36387  erng1r  36423  tendocnv  36450  dvalveclem  36454  dva0g  36456  dvhgrp  36536  dvh0g  36540  dvhopN  36545  cdlemn3  36626  cdlemn8  36633  cdlemn9  36634  dihordlem7b  36644  dihopelvalcpre  36677  dihmeetlem1N  36719  dihglblem5apreN  36720  lcfrlem13  36984  hvmapclN  37193  hvmapcl2  37195
  Copyright terms: Public domain W3C validator