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

Theorem f1of 5750
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 5749 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5715 . 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 5523   -1-1->wf1 5524   -1-1-onto->wf1o 5526
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 5532  df-f1o 5534
This theorem is referenced by:  f1ofn  5751  f1ompt  5975  f1oresrab  5985  fsn  5991  fsnunf  6026  f1ocnvfv1  6093  f1ocnvfv2  6094  f1ocnvdm  6099  fcof1o  6107  fveqf1o  6110  isocnv  6131  isocnv3  6133  isores2  6134  isotr  6137  isofr2  6145  isopolem  6146  isosolem  6148  f1oiso2  6153  weniso  6155  f1ofveu  6196  f1oexrnex  6638  f1oabexg  6647  wemoiso  6673  suppsnop  6815  smoiso  6934  mapsn  7365  ralxpmap  7373  f1oen2g  7437  en1  7487  enfixsn  7531  mapen  7586  ac6sfi  7668  domunfican  7696  fiint  7700  mapfienlem1  7766  mapfienlem2  7767  mapfienlem3  7768  mapfien  7769  supisoex  7833  supiso  7834  ordiso2  7841  ordtypelem10  7853  hartogslem1  7868  unxpwdom2  7915  cantnfle  7991  cantnfp1lem3  8000  cantnflem1b  8006  cantnflem1d  8008  cantnflem1  8009  cantnfleOLD  8021  cantnfp1lem3OLD  8026  cantnflem1bOLD  8029  cantnflem1dOLD  8031  cantnflem1OLD  8032  mapfienOLD  8039  cnfcomlem  8044  cnfcom  8045  cnfcom2lem  8046  cnfcom2  8047  cnfcom3lem  8048  cnfcom3  8049  cnfcom3clem  8050  cnfcomlemOLD  8052  cnfcomOLD  8053  cnfcom2lemOLD  8054  cnfcom2OLD  8055  cnfcom3lemOLD  8056  cnfcom3OLD  8057  cnfcom3clemOLD  8058  infxpenlem  8292  infxpenc  8296  infxpenc2lem2  8298  infxpencOLD  8301  infxpenc2lem2OLD  8302  fseqenlem1  8306  acndom  8333  acndom2  8336  infpwfien  8344  iunfictbso  8396  infmap2  8499  ackbij2lem2  8521  infpssrlem3  8586  infpssrlem4  8587  fin23lem30  8623  isf32lem6  8639  isf32lem7  8640  isf32lem8  8641  enfin1ai  8665  axcc3  8719  axcclem  8738  ttukeylem7  8796  fpwwe2lem6  8914  fpwwe2lem7  8915  fpwwe2lem9  8917  canthp1lem2  8932  canthp1  8933  pwfseqlem4a  8940  pwfseqlem5  8942  dfle2  11236  axdc4uzlem  11922  seqf1olem1  11963  seqf1olem2  11964  seqf1o  11965  hashkf  12223  hasheqf1oi  12240  hashcl  12244  hashgadd  12259  hashfacen  12326  hashf1lem1  12327  fz1isolem  12333  seqcoll  12335  seqcoll2  12336  snopiswrd  12362  cnrecnv  12773  sumeq2ii  13289  summolem3  13310  summolem2a  13311  fsum  13316  fsumf1o  13319  fsumss  13321  fsumcl2lem  13327  fsumadd  13334  fsummulc2  13370  fsumrelem  13389  ackbijnn  13410  sadcaddlem  13772  sadadd2lem  13774  sadadd3  13776  sadaddlem  13781  sadasslem  13785  sadeq  13787  phimullem  13973  eulerthlem1  13975  eulerthlem2  13976  unbenlem  14088  vdwlem8  14168  0ram  14200  wunndx  14309  xpsaddlem  14633  xpsvsca  14637  xpsle  14639  idfucl  14911  setccatid  15072  setcinv  15078  catcisolem  15094  yonffthlem  15212  mhmf1o  15593  gsumpropd2lem  15625  gsumws1  15637  idghm  15882  ghmf1o  15896  symgval  16004  symgbas  16005  elsymgbas  16007  symgbasf  16009  symgbasfi  16011  symg1bas  16021  symggrp  16025  symgid  16026  lactghmga  16029  symgfixf1  16063  f1omvdmvd  16069  f1omvdconj  16072  f1omvdco2  16074  pmtrfconj  16092  symggen  16096  pmtrdifellem1  16102  pmtrdifellem2  16103  psgnunilem1  16119  gsumval3eu  16503  gsumval3OLD  16504  gsumval3lem1  16505  gsumval3  16507  gsumzf1o  16513  gsumzf1oOLD  16516  gsumconst  16550  gsumsub  16570  gsumsubOLD  16571  gsumcom2  16590  dprdfsub  16634  dprdfsubOLD  16641  dprdf1o  16652  dprdsn  16656  ablfaclem2  16710  srngcl  17064  lmhmf1o  17251  fidomndrnglem  17502  psrass1lem  17571  psrnegcl  17591  psrlinv  17592  coe1f2  17790  coe1add  17842  evls1rhmlem  17882  evl1sca  17894  pf1ind  17915  gsumfsum  18005  zntoslem  18115  frgpcyg  18132  islinds2  18368  lindsmm  18383  mdetleib2  18527  mdetrsca  18542  mdetralt  18547  mdetunilem7  18557  mdetunilem9  18559  ssidcn  18992  hausdiag  19351  hmphdis  19502  indishmph  19504  cmphaushmeo  19506  ordthmeolem  19507  txhmeo  19509  pt1hmeo  19512  qtopf1  19522  ufldom  19668  symgtgp  19805  tsmsf1o  19852  iducn  19991  imasdsf1olem  20081  xpsdsval  20089  imasf1obl  20196  icchmeo  20646  iccpnfcnv  20649  xrhmeo  20651  cnheiborlem  20659  ovolctb  21106  ovoliunlem1  21118  ovoliunlem2  21119  iunmbl2  21172  dyadmbl  21214  vitalilem2  21223  vitalilem3  21224  vitalilem4  21225  vitalilem5  21226  mbfid  21248  dvid  21526  dvexp  21561  dvcnvlem  21582  dvcnv  21583  dvcnvrelem2  21624  dvcnvre  21625  efcvx  22048  reefgim  22049  efif1olem4  22135  eff1olem  22138  logrncl  22153  relogcl  22161  dvrelog  22216  relogcn  22217  logcn  22226  logf1o2  22229  dvlog  22230  dvlog2  22232  advlog  22233  advlogexp  22234  logtayl  22239  logccv  22242  dvcxp1  22314  loglesqr  22330  asinrebnd  22430  dvatan  22464  efrlim  22497  amgmlem  22517  wilthlem2  22541  wilthlem3  22542  sqff1o  22654  lgsqrlem4  22817  logdivsum  22916  log2sumbnd  22927  f1otrg  23270  f1otrge  23271  axlowdimlem10  23350  axcontlem5  23367  axcontlem10  23372  umgra1  23413  iseupa  23739  eupatrl  23742  eupa0  23748  eupares  23749  eupap1  23750  eupath2lem3  23753  grposn  23855  ginvsn  23989  dmadjrn  25452  unopnorm  25474  unopadj  25476  unoplin  25477  counop  25478  idcnop  25538  idhmop  25539  unopbd  25572  bracnln  25666  cnvbraval  25667  leopnmid  25695  nmopleid  25696  hmopidmch  25710  hmopidmpj  25711  disjrdx  26085  isoun  26149  fcobij  26177  fcobijfs  26178  abliso  26305  tpr2rico  26488  xrge0iifmhm  26515  xrge0pluscn  26516  rrhre  26593  esumf1o  26650  volmeas  26792  eulerpartgbij  26900  eulerpartlemmf  26903  eulerpartlemgvv  26904  eulerpartlemgf  26907  eulerpartlemgs2  26908  eulerpartlemn  26909  ballotlemsima  27043  lgamcvg2  27186  deranglem  27199  derangsn  27203  derangenlem  27204  subfacp1lem4  27216  subfacp1lem5  27217  subfacp1lem6  27218  cvmfolem  27313  cvmliftlem6  27324  ghomsn  27452  prodeq2ii  27571  prodmolem3  27591  prodmolem2a  27592  fprod  27599  fprodf1o  27604  fprodss  27606  fprodser  27607  fprodcl2lem  27608  fprodmul  27616  fproddiv  27617  fprodn0  27635  mblfinlem2  28578  dvasin  28629  f1ocan1fv  28769  metf1o  28800  ismtyval  28848  isismty  28849  ismtyima  28851  ismtyhmeolem  28852  ismtybndlem  28854  ismrer1  28886  reheibor  28887  rngoisocnv  28936  mapfzcons  29201  mzpresrename  29236  diophrw  29246  eldioph2  29249  diophren  29301  kelac1  29565  imasgim  29604  lnrfg  29624  stoweidlem27  29971  stoweidlem31  29975  stoweidlem39  29983  mat1dimelbas  31034  mat1dimmul  31039  lflnegl  33060  lautset  34065  islaut  34066  lautcl  34070  lautco  34080  pautsetN  34081  ispautN  34082  ldilco  34099  ltrncoidN  34111  ltrncoval  34128  trlcoabs2N  34705  trlcoat  34706  trlcone  34711  cdlemg47a  34717  cdlemg46  34718  cdlemg47  34719  trljco  34723  tgrpgrplem  34732  tendoidcl  34752  tendo0co2  34771  tendo0pl  34774  cdlemi2  34802  cdlemk2  34815  cdlemk4  34817  cdlemk8  34821  cdlemkid2  34907  cdlemk45  34930  cdlemk53b  34939  cdlemk53  34940  cdlemk55a  34942  erng1r  34978  tendocnv  35005  dvalveclem  35009  dva0g  35011  dvhgrp  35091  dvh0g  35095  dvhopN  35100  cdlemn3  35181  cdlemn8  35188  cdlemn9  35189  dihordlem7b  35199  dihopelvalcpre  35232  dihmeetlem1N  35274  dihglblem5apreN  35275  lcfrlem13  35539  hvmapclN  35748  hvmapcl2  35750
  Copyright terms: Public domain W3C validator