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

Theorem f1of 5814
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 5813 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5779 . 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 5582   -1-1->wf1 5583   -1-1-onto->wf1o 5585
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 5591  df-f1o 5593
This theorem is referenced by:  f1ofn  5815  f1ompt  6041  f1oresrab  6051  fsn  6057  fsnunf  6097  f1ocnvfv1  6168  f1ocnvfv2  6169  f1ocnvdm  6174  fcof1oinvd  6182  fveqf1o  6191  isocnv  6212  isocnv3  6214  isores2  6215  isotr  6218  isofr2  6226  isopolem  6227  isosolem  6229  f1oiso2  6234  weniso  6236  f1ofveu  6277  f1oexrnex  6730  f1oabexg  6740  wemoiso  6766  suppsnop  6912  smoiso  7030  mapsn  7457  ralxpmap  7465  f1oen2g  7529  en1  7579  enfixsn  7623  mapen  7678  ac6sfi  7760  domunfican  7789  fiint  7793  mapfienlem1  7860  mapfienlem2  7861  mapfienlem3  7862  mapfien  7863  supisoex  7928  supiso  7929  ordiso2  7936  ordtypelem10  7948  hartogslem1  7963  unxpwdom2  8010  cantnfle  8086  cantnfp1lem3  8095  cantnflem1b  8101  cantnflem1d  8103  cantnflem1  8104  cantnfleOLD  8116  cantnfp1lem3OLD  8121  cantnflem1bOLD  8124  cantnflem1dOLD  8126  cantnflem1OLD  8127  mapfienOLD  8134  cnfcomlem  8139  cnfcom  8140  cnfcom2lem  8141  cnfcom2  8142  cnfcom3lem  8143  cnfcom3  8144  cnfcom3clem  8145  cnfcomlemOLD  8147  cnfcomOLD  8148  cnfcom2lemOLD  8149  cnfcom2OLD  8150  cnfcom3lemOLD  8151  cnfcom3OLD  8152  cnfcom3clemOLD  8153  infxpenlem  8387  infxpenc  8391  infxpenc2lem2  8393  infxpencOLD  8396  infxpenc2lem2OLD  8397  fseqenlem1  8401  acndom  8428  acndom2  8431  infpwfien  8439  iunfictbso  8491  infmap2  8594  ackbij2lem2  8616  infpssrlem3  8681  infpssrlem4  8682  fin23lem30  8718  isf32lem6  8734  isf32lem7  8735  isf32lem8  8736  enfin1ai  8760  axcc3  8814  axcclem  8833  ttukeylem7  8891  fpwwe2lem6  9009  fpwwe2lem7  9010  fpwwe2lem9  9012  canthp1lem2  9027  canthp1  9028  pwfseqlem4a  9035  pwfseqlem5  9037  dfle2  11349  axdc4uzlem  12056  seqf1olem1  12110  seqf1olem2  12111  seqf1o  12112  hashkf  12371  hasheqf1oi  12388  hashcl  12392  hashgadd  12409  hashfacen  12465  hashf1lem1  12466  fz1isolem  12472  seqcoll  12474  seqcoll2  12475  snopiswrd  12518  cnrecnv  12957  sumeq2ii  13474  summolem3  13495  summolem2a  13496  fsum  13501  fsumf1o  13504  fsumss  13506  fsumcl2lem  13512  fsumadd  13520  fsummulc2  13558  fsumrelem  13580  ackbijnn  13599  sadcaddlem  13962  sadadd2lem  13964  sadadd3  13966  sadaddlem  13971  sadasslem  13975  sadeq  13977  phimullem  14164  eulerthlem1  14166  eulerthlem2  14167  unbenlem  14281  vdwlem8  14361  0ram  14393  wunndx  14502  xpsaddlem  14826  xpsvsca  14830  xpsle  14832  idfucl  15104  setccatid  15265  setcinv  15271  catcisolem  15287  yonffthlem  15405  mhmf1o  15786  gsumpropd2lem  15818  gsumws1  15830  idghm  16077  ghmf1o  16091  symgval  16199  symgbas  16200  elsymgbas  16202  symgbasf  16204  symgbasfi  16206  symg1bas  16216  symggrp  16220  symgid  16221  lactghmga  16224  symgfixf1  16258  f1omvdmvd  16264  f1omvdconj  16267  f1omvdco2  16269  pmtrfconj  16287  symggen  16291  pmtrdifellem1  16297  pmtrdifellem2  16298  psgnunilem1  16314  gsumval3eu  16698  gsumval3OLD  16699  gsumval3lem1  16700  gsumval3  16702  gsumzf1o  16708  gsumzf1oOLD  16711  gsumconst  16745  gsumsub  16765  gsumsubOLD  16766  gsumcom2  16794  dprdfsub  16851  dprdfsubOLD  16858  dprdf1o  16869  dprdsn  16873  ablfaclem2  16927  srngcl  17287  lmhmf1o  17475  fidomndrnglem  17726  psrass1lem  17800  psrnegcl  17820  psrlinv  17821  coe1f2  18019  coe1add  18076  evls1rhmlem  18129  evl1sca  18141  pf1ind  18162  gsumfsum  18252  zntoslem  18362  frgpcyg  18379  islinds2  18615  lindsmm  18630  mat1dimelbas  18740  mat1dimmul  18745  mat1f  18751  mdetleib2  18857  mdetrsca  18872  mdetralt  18877  mdetunilem7  18887  mdetunilem9  18889  ssidcn  19522  hausdiag  19881  hmphdis  20032  indishmph  20034  cmphaushmeo  20036  ordthmeolem  20037  txhmeo  20039  pt1hmeo  20042  qtopf1  20052  ufldom  20198  symgtgp  20335  tsmsf1o  20382  iducn  20521  imasdsf1olem  20611  xpsdsval  20619  imasf1obl  20726  icchmeo  21176  iccpnfcnv  21179  xrhmeo  21181  cnheiborlem  21189  ovolctb  21636  ovoliunlem1  21648  ovoliunlem2  21649  iunmbl2  21702  dyadmbl  21744  vitalilem2  21753  vitalilem3  21754  vitalilem4  21755  vitalilem5  21756  mbfid  21778  dvid  22056  dvexp  22091  dvcnvlem  22112  dvcnv  22113  dvcnvrelem2  22154  dvcnvre  22155  efcvx  22578  reefgim  22579  efif1olem4  22665  eff1olem  22668  logrncl  22683  relogcl  22691  dvrelog  22746  relogcn  22747  logcn  22756  logf1o2  22759  dvlog  22760  dvlog2  22762  advlog  22763  advlogexp  22764  logtayl  22769  logccv  22772  dvcxp1  22844  loglesqrt  22860  asinrebnd  22960  dvatan  22994  efrlim  23027  amgmlem  23047  wilthlem2  23071  wilthlem3  23072  sqff1o  23184  lgsqrlem4  23347  logdivsum  23446  log2sumbnd  23457  isismt  23649  motcl  23654  motco  23655  cnvmot  23656  motgrp  23658  motcgrg  23659  motcgr3  23660  f1otrg  23850  f1otrge  23851  axlowdimlem10  23930  axcontlem5  23947  axcontlem10  23952  umgra1  24002  iseupa  24641  eupatrl  24644  eupa0  24650  eupares  24651  eupap1  24652  eupath2lem3  24655  grposn  24893  ginvsn  25027  dmadjrn  26490  unopnorm  26512  unopadj  26514  unoplin  26515  counop  26516  idcnop  26576  idhmop  26577  unopbd  26610  bracnln  26704  cnvbraval  26705  leopnmid  26733  nmopleid  26734  hmopidmch  26748  hmopidmpj  26749  disjrdx  27123  isoun  27192  fcobij  27220  fcobijfs  27221  abliso  27348  tpr2rico  27530  xrge0iifmhm  27557  xrge0pluscn  27558  rrhre  27635  esumf1o  27701  volmeas  27843  eulerpartgbij  27951  eulerpartlemmf  27954  eulerpartlemgvv  27955  eulerpartlemgf  27958  eulerpartlemgs2  27959  eulerpartlemn  27960  ballotlemsima  28094  lgamcvg2  28237  deranglem  28250  derangsn  28254  derangenlem  28255  subfacp1lem4  28267  subfacp1lem5  28268  subfacp1lem6  28269  cvmfolem  28364  cvmliftlem6  28375  ghomsn  28503  prodeq2ii  28622  prodmolem3  28642  prodmolem2a  28643  fprod  28650  fprodf1o  28655  fprodss  28657  fprodser  28658  fprodcl2lem  28659  fprodmul  28667  fproddiv  28668  fprodn0  28686  mblfinlem2  29629  dvasin  29680  f1ocan1fv  29820  metf1o  29851  ismtyval  29899  isismty  29900  ismtyima  29902  ismtyhmeolem  29903  ismtybndlem  29905  ismrer1  29937  reheibor  29938  rngoisocnv  29987  mapfzcons  30252  mzpresrename  30287  diophrw  30296  eldioph2  30299  diophren  30351  kelac1  30613  imasgim  30652  lnrfg  30672  stoweidlem27  31327  stoweidlem31  31331  stoweidlem39  31339  fourierdlem20  31427  fourierdlem50  31457  fourierdlem52  31459  fourierdlem54  31461  fourierdlem64  31471  fourierdlem76  31483  fourierdlem102  31509  fourierdlem114  31521  lflnegl  33873  lautset  34878  islaut  34879  lautcl  34883  lautco  34893  pautsetN  34894  ispautN  34895  ldilco  34912  ltrncoidN  34924  ltrncoval  34941  trlcoabs2N  35518  trlcoat  35519  trlcone  35524  cdlemg47a  35530  cdlemg46  35531  cdlemg47  35532  trljco  35536  tgrpgrplem  35545  tendoidcl  35565  tendo0co2  35584  tendo0pl  35587  cdlemi2  35615  cdlemk2  35628  cdlemk4  35630  cdlemk8  35634  cdlemkid2  35720  cdlemk45  35743  cdlemk53b  35752  cdlemk53  35753  cdlemk55a  35755  erng1r  35791  tendocnv  35818  dvalveclem  35822  dva0g  35824  dvhgrp  35904  dvh0g  35908  dvhopN  35913  cdlemn3  35994  cdlemn8  36001  cdlemn9  36002  dihordlem7b  36012  dihopelvalcpre  36045  dihmeetlem1N  36087  dihglblem5apreN  36088  lcfrlem13  36352  hvmapclN  36561  hvmapcl2  36563
  Copyright terms: Public domain W3C validator