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

Theorem f1of 5488
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 5487 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5453 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
31, 2syl 15 1  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   -->wf 5267   -1-1->wf1 5268   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1ofn  5489  f1oabexg  5500  f1ompt  5698  fsn  5712  fsnunf  5734  f1ocnvfv1  5808  f1ocnvfv2  5809  f1ocnvdm  5812  fcof1o  5819  fveqf1o  5822  isocnv  5843  isocnv3  5845  isores2  5846  isotr  5849  isofr2  5857  isopolem  5858  isosolem  5860  f1oiso2  5865  weniso  5868  wemoiso  5871  f1ofveu  6355  smoiso  6395  mapsn  6825  f1oen2g  6894  en1  6944  mapen  7041  ac6sfi  7117  domunfican  7145  fiint  7149  supisoex  7238  supiso  7239  ordiso2  7246  ordtypelem10  7258  hartogslem1  7273  unxpwdom2  7318  cantnfle  7388  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  mapfien  7415  cnfcomlem  7418  cnfcom  7419  cnfcom2lem  7420  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  cnfcom3clem  7424  infxpenlem  7657  infxpenc  7661  infxpenc2lem2  7663  fseqenlem1  7667  acndom  7694  acndom2  7697  infpwfien  7705  iunfictbso  7757  infmap2  7860  ackbij2lem2  7882  infpssrlem3  7947  infpssrlem4  7948  fin23lem30  7984  isf32lem6  8000  isf32lem7  8001  isf32lem8  8002  enfin1ai  8026  axcc3  8080  axcclem  8099  ttukeylem7  8158  fpwwe2lem6  8273  fpwwe2lem7  8274  fpwwe2lem9  8276  canthp1lem2  8291  canthp1  8292  pwfseqlem4a  8299  pwfseqlem5  8301  dfle2  10497  axdc4uzlem  11060  seqf1olem1  11101  seqf1olem2  11102  seqf1o  11103  hashkf  11355  hashcl  11366  hashgadd  11375  hashfacen  11408  hashf1lem1  11409  fz1isolem  11415  seqcoll  11417  seqcoll2  11418  s1cl  11457  cnrecnv  11666  sumeq2ii  12182  summolem3  12203  summolem2a  12204  fsum  12209  fsumf1o  12212  fsumss  12214  fsumcl2lem  12220  fsumadd  12227  fsummulc2  12262  fsumrelem  12281  ackbijnn  12302  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  sadaddlem  12673  sadasslem  12677  sadeq  12679  phimullem  12863  eulerthlem1  12865  eulerthlem2  12866  unbenlem  12971  vdwlem8  13051  0ram  13083  wunndx  13180  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  idfucl  13771  setccatid  13932  setcinv  13938  catcisolem  13954  yonffthlem  14072  gsumws1  14478  idghm  14714  ghmf1o  14728  symgval  14787  symgbas  14788  elsymgbas  14790  symggrp  14796  symgid  14797  lactghmga  14800  gsumval3eu  15206  gsumval3  15207  gsumzf1o  15212  gsumconst  15225  gsumsub  15235  gsumcom2  15242  dprdfsub  15272  dprdf1o  15283  dprdsn  15287  ablfaclem2  15337  srngcl  15636  lmhmf1o  15819  fidomndrnglem  16063  psrass1lem  16139  psrnegcl  16157  psrlinv  16158  coe1f2  16306  coe1add  16357  gsumfsum  16455  zntoslem  16526  frgpcyg  16543  ssidcn  17001  hausdiag  17355  hmphdis  17503  indishmph  17505  cmphaushmeo  17507  ordthmeolem  17508  txhmeo  17510  pt1hmeo  17513  qtopf1  17523  ufldom  17673  symgtgp  17800  tsmsf1o  17843  imasdsf1olem  17953  xpsdsval  17961  imasf1obl  18050  icchmeo  18455  iccpnfcnv  18458  xrhmeo  18460  cnheiborlem  18468  ovolctb  18865  ovoliunlem1  18877  ovoliunlem2  18878  iunmbl2  18930  dyadmbl  18971  vitalilem2  18980  vitalilem3  18981  vitalilem4  18982  vitalilem5  18983  mbfid  19007  dvid  19283  dvexp  19318  dvcnvlem  19339  dvcnv  19340  dvcnvrelem2  19381  dvcnvre  19382  evl1rhm  19428  evl1sca  19429  pf1ind  19454  efcvx  19841  reefgim  19842  resinf1o  19914  efif1olem4  19923  eff1olem  19926  logrncl  19941  relogcl  19948  dvrelog  20000  relogcn  20001  logcn  20010  logf1o2  20013  dvlog  20014  dvlog2  20016  advlog  20017  advlogexp  20018  logtayl  20023  logccv  20026  dvcxp1  20098  loglesqr  20114  asinrebnd  20213  dvatan  20247  efrlim  20280  amgmlem  20300  wilthlem2  20323  wilthlem3  20324  sqff1o  20436  lgsqrlem4  20599  logdivsum  20698  log2sumbnd  20709  grposn  20898  ginvsn  21032  dmadjrn  22491  unopnorm  22513  unopadj  22515  unoplin  22516  counop  22517  idcnop  22577  idhmop  22578  unopbd  22611  bracnln  22705  cnvbraval  22706  leopnmid  22734  nmopleid  22735  hmopidmch  22749  hmopidmpj  22750  ballotlemsima  23090  ballotlem7  23110  isoun  23257  tpr2rico  23311  xrge0iifmhm  23336  xrge0pluscn  23337  disjrdx  23385  gsumpropd2lem  23394  esumf1o  23444  deranglem  23712  derangsn  23716  derangenlem  23717  subfacp1lem4  23729  subfacp1lem5  23730  subfacp1lem6  23731  cvmfolem  23825  cvmliftlem6  23836  umgra1  23893  iseupa  23896  eupa0  23913  eupares  23914  eupap1  23915  eupath2lem3  23918  ghomsn  24010  cprodeq2ii  24135  prodmolem3  24156  prodmolem2a  24157  fprod  24164  fprodf1o  24172  axlowdimlem10  24651  axcontlem5  24668  axcontlem10  24673  dvreasin  25026  scprefat  25174  cbicp  25269  isoriso  25315  oriso  25317  dispos  25390  hmeogrpi  25639  1alg  25825  idfisf  25944  idsubfun  25961  idcatfun  26044  1iskle  26092  phckle  26130  psckle  26131  pgapspf  26155  f1ocan1fv  26497  metf1o  26572  ismtyval  26627  isismty  26628  ismtyima  26630  ismtyhmeolem  26631  ismtybndlem  26633  ismrer1  26665  reheibor  26666  rngoisocnv  26715  ralxpmap  26864  mapfzcons  26896  mzpresrename  26931  diophrw  26941  eldioph2  26944  diophren  26999  kelac1  27264  enfixsn  27360  imasgim  27367  islinds2  27386  lindsmm  27401  lnrfg  27426  f1omvdmvd  27489  f1omvdconj  27492  f1omvdco2  27494  pmtrfconj  27510  symggen  27514  psgnunilem1  27519  stoweidlem27  27879  stoweidlem31  27883  stoweidlem39  27891  eupatrl  28385  lflnegl  29888  lautset  30893  islaut  30894  lautcl  30898  lautco  30908  pautsetN  30909  ispautN  30910  ldilco  30927  ltrncoidN  30939  ltrncoval  30956  trlcoabs2N  31533  trlcoat  31534  trlcone  31539  cdlemg47a  31545  cdlemg46  31546  cdlemg47  31547  trljco  31551  tgrpgrplem  31560  tendoidcl  31580  tendo0co2  31599  tendo0pl  31602  cdlemi2  31630  cdlemk2  31643  cdlemk4  31645  cdlemk8  31649  cdlemkid2  31735  cdlemk45  31758  cdlemk53b  31767  cdlemk53  31768  cdlemk55a  31770  erng1r  31806  tendocnv  31833  dvalveclem  31837  dva0g  31839  dvhgrp  31919  dvh0g  31923  dvhopN  31928  cdlemn3  32009  cdlemn8  32016  cdlemn9  32017  dihordlem7b  32027  dihopelvalcpre  32060  dihmeetlem1N  32102  dihglblem5apreN  32103  lcfrlem13  32367  hvmapclN  32576  hvmapcl2  32578
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 177  df-an 360  df-f1 5276  df-f1o 5278
  Copyright terms: Public domain W3C validator