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

Theorem f1of 5666
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 5665 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5631 . 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 5442   -1-1->wf1 5443   -1-1-onto->wf1o 5445
This theorem is referenced by:  f1ofn  5667  f1oabexg  5678  f1ompt  5883  fsn  5898  fsnunf  5923  f1ocnvfv1  6006  f1ocnvfv2  6007  f1ocnvdm  6010  fcof1o  6018  fveqf1o  6021  isocnv  6042  isocnv3  6044  isores2  6045  isotr  6048  isofr2  6056  isopolem  6057  isosolem  6059  f1oiso2  6064  weniso  6067  wemoiso  6070  f1ofveu  6576  smoiso  6616  mapsn  7047  f1oen2g  7116  en1  7166  mapen  7263  ac6sfi  7343  domunfican  7371  fiint  7375  supisoex  7468  supiso  7469  ordiso2  7476  ordtypelem10  7488  hartogslem1  7503  unxpwdom2  7548  cantnfle  7618  cantnfp1lem3  7628  cantnflem1b  7634  cantnflem1d  7636  cantnflem1  7637  mapfien  7645  cnfcomlem  7648  cnfcom  7649  cnfcom2lem  7650  cnfcom2  7651  cnfcom3lem  7652  cnfcom3  7653  cnfcom3clem  7654  infxpenlem  7887  infxpenc  7891  infxpenc2lem2  7893  fseqenlem1  7897  acndom  7924  acndom2  7927  infpwfien  7935  iunfictbso  7987  infmap2  8090  ackbij2lem2  8112  infpssrlem3  8177  infpssrlem4  8178  fin23lem30  8214  isf32lem6  8230  isf32lem7  8231  isf32lem8  8232  enfin1ai  8256  axcc3  8310  axcclem  8329  ttukeylem7  8387  fpwwe2lem6  8502  fpwwe2lem7  8503  fpwwe2lem9  8505  canthp1lem2  8520  canthp1  8521  pwfseqlem4a  8528  pwfseqlem5  8530  dfle2  10732  axdc4uzlem  11313  seqf1olem1  11354  seqf1olem2  11355  seqf1o  11356  hashkf  11612  hasheqf1oi  11627  hashcl  11631  hashgadd  11643  hashfacen  11695  hashf1lem1  11696  fz1isolem  11702  seqcoll  11704  seqcoll2  11705  s1cl  11747  cnrecnv  11962  sumeq2ii  12479  summolem3  12500  summolem2a  12501  fsum  12506  fsumf1o  12509  fsumss  12511  fsumcl2lem  12517  fsumadd  12524  fsummulc2  12559  fsumrelem  12578  ackbijnn  12599  sadcaddlem  12961  sadadd2lem  12963  sadadd3  12965  sadaddlem  12970  sadasslem  12974  sadeq  12976  phimullem  13160  eulerthlem1  13162  eulerthlem2  13163  unbenlem  13268  vdwlem8  13348  0ram  13380  wunndx  13477  xpsaddlem  13792  xpsvsca  13796  xpsle  13798  idfucl  14070  setccatid  14231  setcinv  14237  catcisolem  14253  yonffthlem  14371  gsumws1  14777  idghm  15013  ghmf1o  15027  symgval  15086  symgbas  15087  elsymgbas  15089  symggrp  15095  symgid  15096  lactghmga  15099  gsumval3eu  15505  gsumval3  15506  gsumzf1o  15511  gsumconst  15524  gsumsub  15534  gsumcom2  15541  dprdfsub  15571  dprdf1o  15582  dprdsn  15586  ablfaclem2  15636  srngcl  15935  lmhmf1o  16114  fidomndrnglem  16358  psrass1lem  16434  psrnegcl  16452  psrlinv  16453  coe1f2  16599  coe1add  16649  gsumfsum  16758  zntoslem  16829  frgpcyg  16846  ssidcn  17311  hausdiag  17669  hmphdis  17820  indishmph  17822  cmphaushmeo  17824  ordthmeolem  17825  txhmeo  17827  pt1hmeo  17830  qtopf1  17840  ufldom  17986  symgtgp  18123  tsmsf1o  18166  iducn  18305  imasdsf1olem  18395  xpsdsval  18403  imasf1obl  18510  icchmeo  18958  iccpnfcnv  18961  xrhmeo  18963  cnheiborlem  18971  ovolctb  19378  ovoliunlem1  19390  ovoliunlem2  19391  iunmbl2  19443  dyadmbl  19484  vitalilem2  19493  vitalilem3  19494  vitalilem4  19495  vitalilem5  19496  mbfid  19520  dvid  19796  dvexp  19831  dvcnvlem  19852  dvcnv  19853  dvcnvrelem2  19894  dvcnvre  19895  evl1rhm  19941  evl1sca  19942  pf1ind  19967  efcvx  20357  reefgim  20358  efif1olem4  20439  eff1olem  20442  logrncl  20457  relogcl  20465  dvrelog  20520  relogcn  20521  logcn  20530  logf1o2  20533  dvlog  20534  dvlog2  20536  advlog  20537  advlogexp  20538  logtayl  20543  logccv  20546  dvcxp1  20618  loglesqr  20634  asinrebnd  20733  dvatan  20767  efrlim  20800  amgmlem  20820  wilthlem2  20844  wilthlem3  20845  sqff1o  20957  lgsqrlem4  21120  logdivsum  21219  log2sumbnd  21230  umgra1  21353  iseupa  21679  eupatrl  21682  eupa0  21688  eupares  21689  eupap1  21690  eupath2lem3  21693  grposn  21795  ginvsn  21929  dmadjrn  23390  unopnorm  23412  unopadj  23414  unoplin  23415  counop  23416  idcnop  23476  idhmop  23477  unopbd  23510  bracnln  23604  cnvbraval  23605  leopnmid  23633  nmopleid  23634  hmopidmch  23648  hmopidmpj  23649  disjrdx  24023  isoun  24081  gsumpropd2lem  24212  tpr2rico  24302  xrge0iifmhm  24317  xrge0pluscn  24318  rrhre  24379  esumf1o  24437  volmeas  24579  ballotlemsima  24765  lgamcvg2  24831  deranglem  24844  derangsn  24848  derangenlem  24849  subfacp1lem4  24861  subfacp1lem5  24862  subfacp1lem6  24863  cvmfolem  24958  cvmliftlem6  24969  ghomsn  25091  prodeq2ii  25231  prodmolem3  25251  prodmolem2a  25252  fprod  25259  fprodf1o  25264  fprodss  25266  fprodser  25267  fprodcl2lem  25268  fprodmul  25276  fproddiv  25277  fprodn0  25295  axlowdimlem10  25882  axcontlem5  25899  axcontlem10  25904  mblfinlem  26234  dvreasin  26280  f1ocan1fv  26419  metf1o  26452  ismtyval  26500  isismty  26501  ismtyima  26503  ismtyhmeolem  26504  ismtybndlem  26506  ismrer1  26538  reheibor  26539  rngoisocnv  26588  ralxpmap  26733  mapfzcons  26763  mzpresrename  26798  diophrw  26808  eldioph2  26811  diophren  26865  kelac1  27129  enfixsn  27225  imasgim  27232  islinds2  27251  lindsmm  27266  lnrfg  27291  f1omvdmvd  27354  f1omvdconj  27357  f1omvdco2  27359  pmtrfconj  27375  symggen  27379  psgnunilem1  27384  stoweidlem27  27743  stoweidlem31  27747  stoweidlem39  27755  lflnegl  29811  lautset  30816  islaut  30817  lautcl  30821  lautco  30831  pautsetN  30832  ispautN  30833  ldilco  30850  ltrncoidN  30862  ltrncoval  30879  trlcoabs2N  31456  trlcoat  31457  trlcone  31462  cdlemg47a  31468  cdlemg46  31469  cdlemg47  31470  trljco  31474  tgrpgrplem  31483  tendoidcl  31503  tendo0co2  31522  tendo0pl  31525  cdlemi2  31553  cdlemk2  31566  cdlemk4  31568  cdlemk8  31572  cdlemkid2  31658  cdlemk45  31681  cdlemk53b  31690  cdlemk53  31691  cdlemk55a  31693  erng1r  31729  tendocnv  31756  dvalveclem  31760  dva0g  31762  dvhgrp  31842  dvh0g  31846  dvhopN  31851  cdlemn3  31932  cdlemn8  31939  cdlemn9  31940  dihordlem7b  31950  dihopelvalcpre  31983  dihmeetlem1N  32025  dihglblem5apreN  32026  lcfrlem13  32290  hvmapclN  32499  hvmapcl2  32501
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 5451  df-f1o 5453
  Copyright terms: Public domain W3C validator