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

Theorem f1of 5797
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 5796 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5762 . 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 5557   -1-1->wf1 5558   -1-1-onto->wf1o 5560
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 190  df-an 377  df-f1 5566  df-f1o 5568
This theorem is referenced by:  f1ofn  5798  f1ompt  6028  f1oresrab  6040  fsn  6046  fsnunf  6087  f1ocnvfv1  6161  f1ocnvfv2  6162  fsnex  6167  f1ocnvdm  6169  fcof1oinvd  6177  fveqf1o  6186  isocnv  6207  isocnv3  6209  isores2  6210  isotr  6213  isofr2  6221  isopolem  6222  isosolem  6224  f1oiso2  6229  weniso  6231  f1ofveu  6271  f1oexrnex  6730  f1oabexg  6740  wemoiso  6766  suppsnop  6916  smoiso  7068  mapsn  7500  ralxpmap  7508  f1oen2g  7573  en1  7623  enfixsn  7668  mapen  7723  ac6sfi  7802  domunfican  7831  fiint  7835  mapfienlem1  7905  mapfienlem2  7906  mapfienlem3  7907  mapfien  7908  supisoex  7977  supiso  7978  ordiso2  8017  ordtypelem10  8029  hartogslem1  8044  unxpwdom2  8090  cantnfle  8163  cantnfp1lem3  8172  cantnflem1b  8178  cantnflem1d  8180  cantnflem1  8181  cnfcomlem  8191  cnfcom  8192  cnfcom2lem  8193  cnfcom2  8194  cnfcom3lem  8195  cnfcom3  8196  cnfcom3clem  8197  infxpenlem  8431  infxpenc  8436  infxpenc2lem2  8438  fseqenlem1  8442  acndom  8469  acndom2  8472  infpwfien  8480  iunfictbso  8532  infmap2  8635  ackbij2lem2  8657  infpssrlem3  8722  infpssrlem4  8723  fin23lem30  8759  isf32lem6  8775  isf32lem7  8776  isf32lem8  8777  enfin1ai  8801  axcc3  8855  axcclem  8874  ttukeylem7  8932  fpwwe2lem6  9047  fpwwe2lem7  9048  fpwwe2lem9  9050  canthp1lem2  9065  canthp1  9066  pwfseqlem4a  9073  pwfseqlem5  9075  dfle2  11436  axdc4uzlem  12189  seqf1olem1  12246  seqf1olem2  12247  seqf1o  12248  hashkf  12511  hasheqf1oi  12528  hashcl  12532  hashgadd  12550  hashfacen  12612  hashf1lem1  12613  fz1isolem  12619  seqcoll  12622  seqcoll2  12623  snopiswrd  12676  cnrecnv  13239  sumeq2ii  13770  summolem3  13791  summolem2a  13792  fsum  13797  fsumf1o  13800  fsumss  13802  fsumcl2lem  13808  fsumadd  13816  fsummulc2  13856  fsumrelem  13878  ackbijnn  13897  prodeq2ii  13978  prodmolem3  13998  prodmolem2a  13999  fprod  14006  fprodf1o  14011  fprodss  14013  fprodser  14014  fprodcl2lem  14015  fprodmul  14025  fproddiv  14026  fprodn0  14044  sadcaddlem  14442  sadadd2lem  14444  sadadd3  14446  sadaddlem  14451  sadasslem  14455  sadeq  14457  phimullem  14738  eulerthlem1  14740  eulerthlem2  14741  unbenlem  14863  vdwlem8  14949  0ram  14989  wunndx  15148  xpsaddlem  15492  xpsvsca  15496  xpsle  15498  idfucl  15797  setccatid  15990  setcinv  15996  catcisolem  16012  estrccatid  16028  funcestrcsetclem7  16042  funcestrcsetclem8  16043  funcsetcestrclem7  16057  funcsetcestrclem8  16058  yonffthlem  16178  gsumpropd2lem  16527  idmhm  16602  mhmf1o  16603  gsumws1  16634  idghm  16909  ghmf1o  16923  symgval  17031  symgbas  17032  elsymgbas  17034  symgbasf  17036  symgbasfi  17038  symg1bas  17048  symggrp  17052  symgid  17053  lactghmga  17056  symgfixf1  17089  f1omvdmvd  17095  f1omvdconj  17098  f1omvdco2  17100  pmtrfconj  17118  symggen  17122  pmtrdifellem1  17128  pmtrdifellem2  17129  psgnunilem1  17145  gsumval3eu  17549  gsumval3lem1  17550  gsumval3  17552  gsumzf1o  17557  gsumconst  17578  gsumsub  17592  gsumcom2  17618  dprdfsub  17665  dprdf1o  17676  dprdsn  17680  ablfaclem2  17730  srngcl  18094  lmhmf1o  18280  fidomndrnglem  18541  psrass1lem  18612  psrnegcl  18631  psrlinv  18632  coe1f2  18813  coe1add  18868  evls1rhmlem  18921  evl1sca  18933  pf1ind  18954  gsumfsum  19045  zntoslem  19138  frgpcyg  19155  islinds2  19382  lindsmm  19397  mat1dimelbas  19507  mat1dimmul  19512  mat1f  19518  mdetleib2  19624  mdetrsca  19639  mdetralt  19644  mdetunilem7  19654  mdetunilem9  19656  ssidcn  20282  hausdiag  20671  hmphdis  20822  indishmph  20824  cmphaushmeo  20826  ordthmeolem  20827  txhmeo  20829  pt1hmeo  20832  qtopf1  20842  ufldom  20988  symgtgp  21127  tsmsf1o  21170  iducn  21309  imasdsf1olem  21399  xpsdsval  21407  imasf1obl  21514  icchmeo  21980  iccpnfcnv  21983  xrhmeo  21985  cnheiborlem  21993  ovolctb  22454  ovoliunlem1  22466  ovoliunlem2  22467  iunmbl2  22522  dyadmbl  22570  vitalilem2  22579  vitalilem3  22580  vitalilem4  22581  vitalilem5  22582  mbfid  22604  dvid  22884  dvexp  22919  dvcnvlem  22940  dvcnv  22941  dvcnvrelem2  22982  dvcnvre  22983  efcvx  23416  reefgim  23417  efif1olem4  23506  eff1olem  23509  logrncl  23529  relogcl  23537  dvrelog  23594  relogcn  23595  logcn  23604  logf1o2  23607  dvlog  23608  dvlog2  23610  advlog  23611  advlogexp  23612  logtayl  23617  logccv  23620  dvcxp1  23692  loglesqrt  23710  asinrebnd  23839  dvatan  23873  efrlim  23907  amgmlem  23927  lgamcvg2  23992  wilthlem2  24006  wilthlem3  24007  sqff1o  24121  lgsqrlem4  24284  logdivsum  24383  log2sumbnd  24394  isismt  24591  motcl  24596  motco  24597  cnvmot  24598  motgrp  24600  motcgrg  24601  f1otrg  24913  f1otrge  24914  axlowdimlem10  24993  axcontlem5  25010  axcontlem10  25015  umgra1  25065  iseupa  25705  eupatrl  25708  eupa0  25714  eupares  25715  eupap1  25716  eupath2lem3  25719  grposn  25955  ginvsn  26089  dmadjrn  27560  unopnorm  27582  unopadj  27584  unoplin  27585  counop  27586  idcnop  27646  idhmop  27647  unopbd  27680  bracnln  27774  cnvbraval  27775  leopnmid  27803  nmopleid  27804  hmopidmch  27818  hmopidmpj  27819  disjrdx  28211  isoun  28290  padct  28315  fcobij  28318  fcobijfs  28319  abliso  28466  symgfcoeu  28615  tpr2rico  28725  xrge0iifmhm  28752  xrge0pluscn  28753  rrhre  28832  esumf1o  28878  volmeas  29060  eulerpartgbij  29211  eulerpartlemmf  29214  eulerpartlemgvv  29215  eulerpartlemgf  29218  eulerpartlemgs2  29219  eulerpartlemn  29220  ballotlemsima  29354  ballotlemsimaOLD  29392  deranglem  29895  derangsn  29899  derangenlem  29900  subfacp1lem4  29912  subfacp1lem5  29913  subfacp1lem6  29914  cvmfolem  30008  cvmliftlem6  30019  ghomsn  30312  poimirlem1  31943  poimirlem2  31944  poimirlem3  31945  poimirlem4  31946  poimirlem6  31948  poimirlem7  31949  poimirlem9  31951  poimirlem11  31953  poimirlem12  31954  poimirlem16  31958  poimirlem17  31959  poimirlem19  31961  poimirlem20  31962  poimirlem22  31964  poimirlem26  31968  poimirlem27  31969  poimirlem28  31970  poimirlem32  31974  mblfinlem2  31980  dvasin  32030  f1ocan1fv  32055  metf1o  32086  ismtyval  32134  isismty  32135  ismtyima  32137  ismtyhmeolem  32138  ismtybndlem  32140  ismrer1  32172  reheibor  32173  rngoisocnv  32222  lflnegl  32644  lautset  33649  islaut  33650  lautcl  33654  lautco  33664  pautsetN  33665  ispautN  33666  ldilco  33683  ltrncoidN  33695  ltrncoval  33712  trlcoabs2N  34291  trlcoat  34292  trlcone  34297  cdlemg47a  34303  cdlemg46  34304  cdlemg47  34305  trljco  34309  tgrpgrplem  34318  tendoidcl  34338  tendo0co2  34357  tendo0pl  34360  cdlemi2  34388  cdlemk2  34401  cdlemk4  34403  cdlemk8  34407  cdlemkid2  34493  cdlemk45  34516  cdlemk53b  34525  cdlemk53  34526  cdlemk55a  34528  erng1r  34564  tendocnv  34591  dvalveclem  34595  dva0g  34597  dvhgrp  34677  dvh0g  34681  dvhopN  34686  cdlemn3  34767  cdlemn8  34774  cdlemn9  34775  dihordlem7b  34785  dihopelvalcpre  34818  dihmeetlem1N  34860  dihglblem5apreN  34861  lcfrlem13  35125  hvmapclN  35334  hvmapcl2  35336  mapfzcons  35560  mzpresrename  35594  diophrw  35603  eldioph2  35606  diophren  35658  kelac1  35923  imasgim  35960  lnrfg  35980  mapsnd  37486  stoweidlem27  37944  stoweidlem31  37949  stoweidlem39  37957  fourierdlem20  38046  fourierdlem50  38077  fourierdlem52  38079  fourierdlem54  38081  fourierdlem64  38091  fourierdlem76  38103  fourierdlem102  38129  fourierdlem114  38141  sge0f1o  38283  nnfoctbdjlem  38354  isomenndlem  38415  ovnsubaddlem1  38455  nnsum3primesprm  38976  upgr1e  39301  upgrres1  39482  umgrres1  39483  mgmhmf1o  40112  idmgmhm  40113  funcringcsetcALTV2lem8  40370  funcringcsetclem8ALTV  40393
  Copyright terms: Public domain W3C validator