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

Theorem f1of 5607
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 5606 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5572 . 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 set class
Syntax hints:    -> wi 4   -->wf 5383   -1-1->wf1 5384   -1-1-onto->wf1o 5386
This theorem is referenced by:  f1ofn  5608  f1oabexg  5619  f1ompt  5823  fsn  5838  fsnunf  5863  f1ocnvfv1  5946  f1ocnvfv2  5947  f1ocnvdm  5950  fcof1o  5958  fveqf1o  5961  isocnv  5982  isocnv3  5984  isores2  5985  isotr  5988  isofr2  5996  isopolem  5997  isosolem  5999  f1oiso2  6004  weniso  6007  wemoiso  6010  f1ofveu  6513  smoiso  6553  mapsn  6984  f1oen2g  7053  en1  7103  mapen  7200  ac6sfi  7280  domunfican  7308  fiint  7312  supisoex  7402  supiso  7403  ordiso2  7410  ordtypelem10  7422  hartogslem1  7437  unxpwdom2  7482  cantnfle  7552  cantnfp1lem3  7562  cantnflem1b  7568  cantnflem1d  7570  cantnflem1  7571  mapfien  7579  cnfcomlem  7582  cnfcom  7583  cnfcom2lem  7584  cnfcom2  7585  cnfcom3lem  7586  cnfcom3  7587  cnfcom3clem  7588  infxpenlem  7821  infxpenc  7825  infxpenc2lem2  7827  fseqenlem1  7831  acndom  7858  acndom2  7861  infpwfien  7869  iunfictbso  7921  infmap2  8024  ackbij2lem2  8046  infpssrlem3  8111  infpssrlem4  8112  fin23lem30  8148  isf32lem6  8164  isf32lem7  8165  isf32lem8  8166  enfin1ai  8190  axcc3  8244  axcclem  8263  ttukeylem7  8321  fpwwe2lem6  8436  fpwwe2lem7  8437  fpwwe2lem9  8439  canthp1lem2  8454  canthp1  8455  pwfseqlem4a  8462  pwfseqlem5  8464  dfle2  10665  axdc4uzlem  11241  seqf1olem1  11282  seqf1olem2  11283  seqf1o  11284  hashkf  11540  hasheqf1oi  11555  hashcl  11559  hashgadd  11571  hashfacen  11623  hashf1lem1  11624  fz1isolem  11630  seqcoll  11632  seqcoll2  11633  s1cl  11675  cnrecnv  11890  sumeq2ii  12407  summolem3  12428  summolem2a  12429  fsum  12434  fsumf1o  12437  fsumss  12439  fsumcl2lem  12445  fsumadd  12452  fsummulc2  12487  fsumrelem  12506  ackbijnn  12527  sadcaddlem  12889  sadadd2lem  12891  sadadd3  12893  sadaddlem  12898  sadasslem  12902  sadeq  12904  phimullem  13088  eulerthlem1  13090  eulerthlem2  13091  unbenlem  13196  vdwlem8  13276  0ram  13308  wunndx  13405  xpsaddlem  13720  xpsvsca  13724  xpsle  13726  idfucl  13998  setccatid  14159  setcinv  14165  catcisolem  14181  yonffthlem  14299  gsumws1  14705  idghm  14941  ghmf1o  14955  symgval  15014  symgbas  15015  elsymgbas  15017  symggrp  15023  symgid  15024  lactghmga  15027  gsumval3eu  15433  gsumval3  15434  gsumzf1o  15439  gsumconst  15452  gsumsub  15462  gsumcom2  15469  dprdfsub  15499  dprdf1o  15510  dprdsn  15514  ablfaclem2  15564  srngcl  15863  lmhmf1o  16042  fidomndrnglem  16286  psrass1lem  16362  psrnegcl  16380  psrlinv  16381  coe1f2  16527  coe1add  16577  gsumfsum  16682  zntoslem  16753  frgpcyg  16770  ssidcn  17234  hausdiag  17591  hmphdis  17742  indishmph  17744  cmphaushmeo  17746  ordthmeolem  17747  txhmeo  17749  pt1hmeo  17752  qtopf1  17762  ufldom  17908  symgtgp  18045  tsmsf1o  18088  iducn  18227  imasdsf1olem  18304  xpsdsval  18312  imasf1obl  18401  icchmeo  18830  iccpnfcnv  18833  xrhmeo  18835  cnheiborlem  18843  ovolctb  19246  ovoliunlem1  19258  ovoliunlem2  19259  iunmbl2  19311  dyadmbl  19352  vitalilem2  19361  vitalilem3  19362  vitalilem4  19363  vitalilem5  19364  mbfid  19388  dvid  19664  dvexp  19699  dvcnvlem  19720  dvcnv  19721  dvcnvrelem2  19762  dvcnvre  19763  evl1rhm  19809  evl1sca  19810  pf1ind  19835  efcvx  20225  reefgim  20226  efif1olem4  20307  eff1olem  20310  logrncl  20325  relogcl  20333  dvrelog  20388  relogcn  20389  logcn  20398  logf1o2  20401  dvlog  20402  dvlog2  20404  advlog  20405  advlogexp  20406  logtayl  20411  logccv  20414  dvcxp1  20486  loglesqr  20502  asinrebnd  20601  dvatan  20635  efrlim  20668  amgmlem  20688  wilthlem2  20712  wilthlem3  20713  sqff1o  20825  lgsqrlem4  20988  logdivsum  21087  log2sumbnd  21098  umgra1  21221  iseupa  21528  eupatrl  21531  eupa0  21537  eupares  21538  eupap1  21539  eupath2lem3  21542  grposn  21644  ginvsn  21778  dmadjrn  23239  unopnorm  23261  unopadj  23263  unoplin  23264  counop  23265  idcnop  23325  idhmop  23326  unopbd  23359  bracnln  23453  cnvbraval  23454  leopnmid  23482  nmopleid  23483  hmopidmch  23497  hmopidmpj  23498  disjrdx  23867  isoun  23923  gsumpropd2lem  24042  tpr2rico  24107  xrge0iifmhm  24122  xrge0pluscn  24123  rrhre  24176  esumf1o  24234  volmeas  24374  ballotlemsima  24545  lgamcvg2  24611  deranglem  24624  derangsn  24628  derangenlem  24629  subfacp1lem4  24641  subfacp1lem5  24642  subfacp1lem6  24643  cvmfolem  24738  cvmliftlem6  24749  ghomsn  24871  prodeq2ii  25011  prodmolem3  25031  prodmolem2a  25032  fprod  25039  fprodf1o  25044  fprodss  25046  fprodser  25047  fprodcl2lem  25048  fprodmul  25056  fproddiv  25057  fprodn0  25075  axlowdimlem10  25597  axcontlem5  25614  axcontlem10  25619  dvreasin  25973  f1ocan1fv  26112  metf1o  26145  ismtyval  26193  isismty  26194  ismtyima  26196  ismtyhmeolem  26197  ismtybndlem  26199  ismrer1  26231  reheibor  26232  rngoisocnv  26281  ralxpmap  26426  mapfzcons  26456  mzpresrename  26491  diophrw  26501  eldioph2  26504  diophren  26558  kelac1  26823  enfixsn  26919  imasgim  26926  islinds2  26945  lindsmm  26960  lnrfg  26985  f1omvdmvd  27048  f1omvdconj  27051  f1omvdco2  27053  pmtrfconj  27069  symggen  27073  psgnunilem1  27078  stoweidlem27  27437  stoweidlem31  27441  stoweidlem39  27449  lflnegl  29242  lautset  30247  islaut  30248  lautcl  30252  lautco  30262  pautsetN  30263  ispautN  30264  ldilco  30281  ltrncoidN  30293  ltrncoval  30310  trlcoabs2N  30887  trlcoat  30888  trlcone  30893  cdlemg47a  30899  cdlemg46  30900  cdlemg47  30901  trljco  30905  tgrpgrplem  30914  tendoidcl  30934  tendo0co2  30953  tendo0pl  30956  cdlemi2  30984  cdlemk2  30997  cdlemk4  30999  cdlemk8  31003  cdlemkid2  31089  cdlemk45  31112  cdlemk53b  31121  cdlemk53  31122  cdlemk55a  31124  erng1r  31160  tendocnv  31187  dvalveclem  31191  dva0g  31193  dvhgrp  31273  dvh0g  31277  dvhopN  31282  cdlemn3  31363  cdlemn8  31370  cdlemn9  31371  dihordlem7b  31381  dihopelvalcpre  31414  dihmeetlem1N  31456  dihglblem5apreN  31457  lcfrlem13  31721  hvmapclN  31930  hvmapcl2  31932
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-f1 5392  df-f1o 5394
  Copyright terms: Public domain W3C validator