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

Theorem f1of 5831
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 5830 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5796 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
31, 2syl 17 1  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   -->wf 5597   -1-1->wf1 5598   -1-1-onto->wf1o 5600
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 188  df-an 372  df-f1 5606  df-f1o 5608
This theorem is referenced by:  f1ofn  5832  f1ompt  6059  f1oresrab  6070  fsn  6076  fsnunf  6117  f1ocnvfv1  6190  f1ocnvfv2  6191  fsnex  6196  f1ocnvdm  6198  fcof1oinvd  6206  fveqf1o  6215  isocnv  6236  isocnv3  6238  isores2  6239  isotr  6242  isofr2  6250  isopolem  6251  isosolem  6253  f1oiso2  6258  weniso  6260  f1ofveu  6300  f1oexrnex  6756  f1oabexg  6766  wemoiso  6792  suppsnop  6939  smoiso  7089  mapsn  7521  ralxpmap  7529  f1oen2g  7593  en1  7643  enfixsn  7687  mapen  7742  ac6sfi  7821  domunfican  7850  fiint  7854  mapfienlem1  7924  mapfienlem2  7925  mapfienlem3  7926  mapfien  7927  supisoex  7996  supiso  7997  ordiso2  8030  ordtypelem10  8042  hartogslem1  8057  unxpwdom2  8103  cantnfle  8175  cantnfp1lem3  8184  cantnflem1b  8190  cantnflem1d  8192  cantnflem1  8193  cnfcomlem  8203  cnfcom  8204  cnfcom2lem  8205  cnfcom2  8206  cnfcom3lem  8207  cnfcom3  8208  cnfcom3clem  8209  infxpenlem  8443  infxpenc  8447  infxpenc2lem2  8449  fseqenlem1  8453  acndom  8480  acndom2  8483  infpwfien  8491  iunfictbso  8543  infmap2  8646  ackbij2lem2  8668  infpssrlem3  8733  infpssrlem4  8734  fin23lem30  8770  isf32lem6  8786  isf32lem7  8787  isf32lem8  8788  enfin1ai  8812  axcc3  8866  axcclem  8885  ttukeylem7  8943  fpwwe2lem6  9059  fpwwe2lem7  9060  fpwwe2lem9  9062  canthp1lem2  9077  canthp1  9078  pwfseqlem4a  9085  pwfseqlem5  9087  dfle2  11446  axdc4uzlem  12192  seqf1olem1  12249  seqf1olem2  12250  seqf1o  12251  hashkf  12514  hasheqf1oi  12531  hashcl  12535  hashgadd  12553  hashfacen  12612  hashf1lem1  12613  fz1isolem  12619  seqcoll  12621  seqcoll2  12622  snopiswrd  12668  cnrecnv  13207  sumeq2ii  13737  summolem3  13758  summolem2a  13759  fsum  13764  fsumf1o  13767  fsumss  13769  fsumcl2lem  13775  fsumadd  13783  fsummulc2  13823  fsumrelem  13845  ackbijnn  13864  prodeq2ii  13945  prodmolem3  13965  prodmolem2a  13966  fprod  13973  fprodf1o  13978  fprodss  13980  fprodser  13981  fprodcl2lem  13982  fprodmul  13992  fproddiv  13993  fprodn0  14011  sadcaddlem  14405  sadadd2lem  14407  sadadd3  14409  sadaddlem  14414  sadasslem  14418  sadeq  14420  phimullem  14696  eulerthlem1  14698  eulerthlem2  14699  unbenlem  14815  vdwlem8  14901  0ram  14941  wunndx  15100  xpsaddlem  15432  xpsvsca  15436  xpsle  15438  idfucl  15737  setccatid  15930  setcinv  15936  catcisolem  15952  estrccatid  15968  funcestrcsetclem7  15982  funcestrcsetclem8  15983  funcsetcestrclem7  15997  funcsetcestrclem8  15998  yonffthlem  16118  gsumpropd2lem  16467  idmhm  16542  mhmf1o  16543  gsumws1  16574  idghm  16849  ghmf1o  16863  symgval  16971  symgbas  16972  elsymgbas  16974  symgbasf  16976  symgbasfi  16978  symg1bas  16988  symggrp  16992  symgid  16993  lactghmga  16996  symgfixf1  17029  f1omvdmvd  17035  f1omvdconj  17038  f1omvdco2  17040  pmtrfconj  17058  symggen  17062  pmtrdifellem1  17068  pmtrdifellem2  17069  psgnunilem1  17085  gsumval3eu  17473  gsumval3lem1  17474  gsumval3  17476  gsumzf1o  17481  gsumconst  17502  gsumsub  17516  gsumcom2  17542  dprdfsub  17589  dprdf1o  17600  dprdsn  17604  ablfaclem2  17654  srngcl  18018  lmhmf1o  18204  fidomndrnglem  18465  psrass1lem  18536  psrnegcl  18555  psrlinv  18556  coe1f2  18737  coe1add  18792  evls1rhmlem  18845  evl1sca  18857  pf1ind  18878  gsumfsum  18969  zntoslem  19058  frgpcyg  19075  islinds2  19302  lindsmm  19317  mat1dimelbas  19427  mat1dimmul  19432  mat1f  19438  mdetleib2  19544  mdetrsca  19559  mdetralt  19564  mdetunilem7  19574  mdetunilem9  19576  ssidcn  20202  hausdiag  20591  hmphdis  20742  indishmph  20744  cmphaushmeo  20746  ordthmeolem  20747  txhmeo  20749  pt1hmeo  20752  qtopf1  20762  ufldom  20908  symgtgp  21047  tsmsf1o  21090  iducn  21229  imasdsf1olem  21319  xpsdsval  21327  imasf1obl  21434  icchmeo  21865  iccpnfcnv  21868  xrhmeo  21870  cnheiborlem  21878  ovolctb  22321  ovoliunlem1  22333  ovoliunlem2  22334  iunmbl2  22387  dyadmbl  22435  vitalilem2  22444  vitalilem3  22445  vitalilem4  22446  vitalilem5  22447  mbfid  22469  dvid  22749  dvexp  22784  dvcnvlem  22805  dvcnv  22806  dvcnvrelem2  22847  dvcnvre  22848  efcvx  23269  reefgim  23270  efif1olem4  23359  eff1olem  23362  logrncl  23382  relogcl  23390  dvrelog  23447  relogcn  23448  logcn  23457  logf1o2  23460  dvlog  23461  dvlog2  23463  advlog  23464  advlogexp  23465  logtayl  23470  logccv  23473  dvcxp1  23545  loglesqrt  23563  asinrebnd  23692  dvatan  23726  efrlim  23760  amgmlem  23780  lgamcvg2  23845  wilthlem2  23859  wilthlem3  23860  sqff1o  23972  lgsqrlem4  24135  logdivsum  24234  log2sumbnd  24245  isismt  24439  motcl  24444  motco  24445  cnvmot  24446  motgrp  24448  motcgrg  24449  f1otrg  24747  f1otrge  24748  axlowdimlem10  24827  axcontlem5  24844  axcontlem10  24849  umgra1  24899  iseupa  25538  eupatrl  25541  eupa0  25547  eupares  25548  eupap1  25549  eupath2lem3  25552  grposn  25788  ginvsn  25922  dmadjrn  27383  unopnorm  27405  unopadj  27407  unoplin  27408  counop  27409  idcnop  27469  idhmop  27470  unopbd  27503  bracnln  27597  cnvbraval  27598  leopnmid  27626  nmopleid  27627  hmopidmch  27641  hmopidmpj  27642  disjrdx  28040  isoun  28122  padct  28150  fcobij  28153  fcobijfs  28154  abliso  28297  symgfcoeu  28447  tpr2rico  28557  xrge0iifmhm  28584  xrge0pluscn  28585  rrhre  28664  esumf1o  28710  volmeas  28893  eulerpartgbij  29031  eulerpartlemmf  29034  eulerpartlemgvv  29035  eulerpartlemgf  29038  eulerpartlemgs2  29039  eulerpartlemn  29040  ballotlemsima  29174  deranglem  29677  derangsn  29681  derangenlem  29682  subfacp1lem4  29694  subfacp1lem5  29695  subfacp1lem6  29696  cvmfolem  29790  cvmliftlem6  29801  ghomsn  30094  poimirlem1  31644  poimirlem2  31645  poimirlem3  31646  poimirlem4  31647  poimirlem6  31649  poimirlem7  31650  poimirlem9  31652  poimirlem11  31654  poimirlem12  31655  poimirlem16  31659  poimirlem17  31660  poimirlem19  31662  poimirlem20  31663  poimirlem22  31665  poimirlem26  31669  poimirlem27  31670  poimirlem28  31671  poimirlem32  31675  mblfinlem2  31681  dvasin  31731  f1ocan1fv  31756  metf1o  31787  ismtyval  31835  isismty  31836  ismtyima  31838  ismtyhmeolem  31839  ismtybndlem  31841  ismrer1  31873  reheibor  31874  rngoisocnv  31923  lflnegl  32350  lautset  33355  islaut  33356  lautcl  33360  lautco  33370  pautsetN  33371  ispautN  33372  ldilco  33389  ltrncoidN  33401  ltrncoval  33418  trlcoabs2N  33997  trlcoat  33998  trlcone  34003  cdlemg47a  34009  cdlemg46  34010  cdlemg47  34011  trljco  34015  tgrpgrplem  34024  tendoidcl  34044  tendo0co2  34063  tendo0pl  34066  cdlemi2  34094  cdlemk2  34107  cdlemk4  34109  cdlemk8  34113  cdlemkid2  34199  cdlemk45  34222  cdlemk53b  34231  cdlemk53  34232  cdlemk55a  34234  erng1r  34270  tendocnv  34297  dvalveclem  34301  dva0g  34303  dvhgrp  34383  dvh0g  34387  dvhopN  34392  cdlemn3  34473  cdlemn8  34480  cdlemn9  34481  dihordlem7b  34491  dihopelvalcpre  34524  dihmeetlem1N  34566  dihglblem5apreN  34567  lcfrlem13  34831  hvmapclN  35040  hvmapcl2  35042  mapfzcons  35266  mzpresrename  35300  diophrw  35309  eldioph2  35312  diophren  35364  kelac1  35626  imasgim  35663  lnrfg  35683  stoweidlem27  37455  stoweidlem31  37460  stoweidlem39  37468  fourierdlem20  37557  fourierdlem50  37587  fourierdlem52  37589  fourierdlem54  37591  fourierdlem64  37601  fourierdlem76  37613  fourierdlem102  37639  fourierdlem114  37651  sge0f1o  37757  nnfoctbdjlem  37801  nnsum3primesprm  38274  mgmhmf1o  38544  idmgmhm  38545  funcringcsetcALTV2lem8  38802  funcringcsetclem8ALTV  38825
  Copyright terms: Public domain W3C validator