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

Theorem f1of 5798
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 5797 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5763 . 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 5566   -1-1->wf1 5567   -1-1-onto->wf1o 5569
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 369  df-f1 5575  df-f1o 5577
This theorem is referenced by:  f1ofn  5799  f1ompt  6029  f1oresrab  6039  fsn  6045  fsnunf  6085  f1ocnvfv1  6157  f1ocnvfv2  6158  f1ocnvdm  6163  fcof1oinvd  6171  fveqf1o  6180  isocnv  6201  isocnv3  6203  isores2  6204  isotr  6207  isofr2  6215  isopolem  6216  isosolem  6218  f1oiso2  6223  weniso  6225  f1ofveu  6265  f1oexrnex  6722  f1oabexg  6732  wemoiso  6758  suppsnop  6905  smoiso  7025  mapsn  7453  ralxpmap  7461  f1oen2g  7525  en1  7575  enfixsn  7619  mapen  7674  ac6sfi  7756  domunfican  7785  fiint  7789  mapfienlem1  7856  mapfienlem2  7857  mapfienlem3  7858  mapfien  7859  supisoex  7924  supiso  7925  ordiso2  7932  ordtypelem10  7944  hartogslem1  7959  unxpwdom2  8006  cantnfle  8081  cantnfp1lem3  8090  cantnflem1b  8096  cantnflem1d  8098  cantnflem1  8099  cantnfleOLD  8111  cantnfp1lem3OLD  8116  cantnflem1bOLD  8119  cantnflem1dOLD  8121  cantnflem1OLD  8122  mapfienOLD  8129  cnfcomlem  8134  cnfcom  8135  cnfcom2lem  8136  cnfcom2  8137  cnfcom3lem  8138  cnfcom3  8139  cnfcom3clem  8140  cnfcomlemOLD  8142  cnfcomOLD  8143  cnfcom2lemOLD  8144  cnfcom2OLD  8145  cnfcom3lemOLD  8146  cnfcom3OLD  8147  cnfcom3clemOLD  8148  infxpenlem  8382  infxpenc  8386  infxpenc2lem2  8388  infxpencOLD  8391  infxpenc2lem2OLD  8392  fseqenlem1  8396  acndom  8423  acndom2  8426  infpwfien  8434  iunfictbso  8486  infmap2  8589  ackbij2lem2  8611  infpssrlem3  8676  infpssrlem4  8677  fin23lem30  8713  isf32lem6  8729  isf32lem7  8730  isf32lem8  8731  enfin1ai  8755  axcc3  8809  axcclem  8828  ttukeylem7  8886  fpwwe2lem6  9002  fpwwe2lem7  9003  fpwwe2lem9  9005  canthp1lem2  9020  canthp1  9021  pwfseqlem4a  9028  pwfseqlem5  9030  dfle2  11356  axdc4uzlem  12077  seqf1olem1  12131  seqf1olem2  12132  seqf1o  12133  hashkf  12392  hasheqf1oi  12409  hashcl  12413  hashgadd  12431  hashfacen  12490  hashf1lem1  12491  fz1isolem  12497  seqcoll  12499  seqcoll2  12500  snopiswrd  12546  cnrecnv  13083  sumeq2ii  13600  summolem3  13621  summolem2a  13622  fsum  13627  fsumf1o  13630  fsumss  13632  fsumcl2lem  13638  fsumadd  13646  fsummulc2  13684  fsumrelem  13706  ackbijnn  13725  prodeq2ii  13805  prodmolem3  13825  prodmolem2a  13826  fprod  13833  fprodf1o  13838  fprodss  13840  fprodser  13841  fprodcl2lem  13842  fprodmul  13850  fproddiv  13851  fprodn0  13868  sadcaddlem  14194  sadadd2lem  14196  sadadd3  14198  sadaddlem  14203  sadasslem  14207  sadeq  14209  phimullem  14396  eulerthlem1  14398  eulerthlem2  14399  unbenlem  14513  vdwlem8  14593  0ram  14625  wunndx  14735  xpsaddlem  15067  xpsvsca  15071  xpsle  15073  idfucl  15372  setccatid  15565  setcinv  15571  catcisolem  15587  estrccatid  15603  funcestrcsetclem7  15617  funcestrcsetclem8  15618  funcsetcestrclem7  15632  funcsetcestrclem8  15633  yonffthlem  15753  gsumpropd2lem  16102  idmhm  16177  mhmf1o  16178  gsumws1  16209  idghm  16484  ghmf1o  16498  symgval  16606  symgbas  16607  elsymgbas  16609  symgbasf  16611  symgbasfi  16613  symg1bas  16623  symggrp  16627  symgid  16628  lactghmga  16631  symgfixf1  16664  f1omvdmvd  16670  f1omvdconj  16673  f1omvdco2  16675  pmtrfconj  16693  symggen  16697  pmtrdifellem1  16703  pmtrdifellem2  16704  psgnunilem1  16720  gsumval3eu  17109  gsumval3OLD  17110  gsumval3lem1  17111  gsumval3  17113  gsumzf1o  17119  gsumzf1oOLD  17122  gsumconst  17155  gsumsub  17174  gsumcom2  17202  dprdfsub  17259  dprdfsubOLD  17266  dprdf1o  17277  dprdsn  17281  ablfaclem2  17335  srngcl  17702  lmhmf1o  17890  fidomndrnglem  18153  psrass1lem  18227  psrnegcl  18247  psrlinv  18248  coe1f2  18446  coe1add  18503  evls1rhmlem  18556  evl1sca  18568  pf1ind  18589  gsumfsum  18682  zntoslem  18771  frgpcyg  18788  islinds2  19018  lindsmm  19033  mat1dimelbas  19143  mat1dimmul  19148  mat1f  19154  mdetleib2  19260  mdetrsca  19275  mdetralt  19280  mdetunilem7  19290  mdetunilem9  19292  ssidcn  19926  hausdiag  20315  hmphdis  20466  indishmph  20468  cmphaushmeo  20470  ordthmeolem  20471  txhmeo  20473  pt1hmeo  20476  qtopf1  20486  ufldom  20632  symgtgp  20769  tsmsf1o  20816  iducn  20955  imasdsf1olem  21045  xpsdsval  21053  imasf1obl  21160  icchmeo  21610  iccpnfcnv  21613  xrhmeo  21615  cnheiborlem  21623  ovolctb  22070  ovoliunlem1  22082  ovoliunlem2  22083  iunmbl2  22136  dyadmbl  22178  vitalilem2  22187  vitalilem3  22188  vitalilem4  22189  vitalilem5  22190  mbfid  22212  dvid  22490  dvexp  22525  dvcnvlem  22546  dvcnv  22547  dvcnvrelem2  22588  dvcnvre  22589  efcvx  23013  reefgim  23014  efif1olem4  23101  eff1olem  23104  logrncl  23124  relogcl  23132  dvrelog  23189  relogcn  23190  logcn  23199  logf1o2  23202  dvlog  23203  dvlog2  23205  advlog  23206  advlogexp  23207  logtayl  23212  logccv  23215  dvcxp1  23287  loglesqrt  23303  asinrebnd  23432  dvatan  23466  efrlim  23500  amgmlem  23520  wilthlem2  23544  wilthlem3  23545  sqff1o  23657  lgsqrlem4  23820  logdivsum  23919  log2sumbnd  23930  isismt  24125  motcl  24130  motco  24131  cnvmot  24132  motgrp  24134  motcgrg  24135  f1otrg  24379  f1otrge  24380  axlowdimlem10  24459  axcontlem5  24476  axcontlem10  24481  umgra1  24531  iseupa  25170  eupatrl  25173  eupa0  25179  eupares  25180  eupap1  25181  eupath2lem3  25184  grposn  25418  ginvsn  25552  dmadjrn  27015  unopnorm  27037  unopadj  27039  unoplin  27040  counop  27041  idcnop  27101  idhmop  27102  unopbd  27135  bracnln  27229  cnvbraval  27230  leopnmid  27258  nmopleid  27259  hmopidmch  27273  hmopidmpj  27274  disjrdx  27664  isoun  27751  padct  27779  fcobij  27782  fcobijfs  27783  abliso  27923  tpr2rico  28132  xrge0iifmhm  28159  xrge0pluscn  28160  rrhre  28236  esumf1o  28282  volmeas  28443  eulerpartgbij  28578  eulerpartlemmf  28581  eulerpartlemgvv  28582  eulerpartlemgf  28585  eulerpartlemgs2  28586  eulerpartlemn  28587  ballotlemsima  28721  lgamcvg2  28864  deranglem  28877  derangsn  28881  derangenlem  28882  subfacp1lem4  28894  subfacp1lem5  28895  subfacp1lem6  28896  cvmfolem  28991  cvmliftlem6  29002  ghomsn  29295  mblfinlem2  30295  dvasin  30346  f1ocan1fv  30460  metf1o  30491  ismtyval  30539  isismty  30540  ismtyima  30542  ismtyhmeolem  30543  ismtybndlem  30545  ismrer1  30577  reheibor  30578  rngoisocnv  30627  mapfzcons  30891  mzpresrename  30925  diophrw  30934  eldioph2  30937  diophren  30989  kelac1  31251  imasgim  31292  lnrfg  31312  stoweidlem27  32051  stoweidlem31  32055  stoweidlem39  32063  fourierdlem20  32151  fourierdlem50  32181  fourierdlem52  32183  fourierdlem54  32185  fourierdlem64  32195  fourierdlem76  32207  fourierdlem102  32233  fourierdlem114  32245  mgmhmf1o  32866  idmgmhm  32867  funcringcsetcALTV2lem8  33124  funcringcsetclem8ALTV  33147  lflnegl  35217  lautset  36222  islaut  36223  lautcl  36227  lautco  36237  pautsetN  36238  ispautN  36239  ldilco  36256  ltrncoidN  36268  ltrncoval  36285  trlcoabs2N  36864  trlcoat  36865  trlcone  36870  cdlemg47a  36876  cdlemg46  36877  cdlemg47  36878  trljco  36882  tgrpgrplem  36891  tendoidcl  36911  tendo0co2  36930  tendo0pl  36933  cdlemi2  36961  cdlemk2  36974  cdlemk4  36976  cdlemk8  36980  cdlemkid2  37066  cdlemk45  37089  cdlemk53b  37098  cdlemk53  37099  cdlemk55a  37101  erng1r  37137  tendocnv  37164  dvalveclem  37168  dva0g  37170  dvhgrp  37250  dvh0g  37254  dvhopN  37259  cdlemn3  37340  cdlemn8  37347  cdlemn9  37348  dihordlem7b  37358  dihopelvalcpre  37391  dihmeetlem1N  37433  dihglblem5apreN  37434  lcfrlem13  37698  hvmapclN  37907  hvmapcl2  37909
  Copyright terms: Public domain W3C validator