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

Theorem f1of 6591
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 6590 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 6551 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wf 6327  1-1wf1 6328  1-1-ontowf1o 6330
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 209  df-an 399  df-f1 6336  df-f1o 6338
This theorem is referenced by:  f1ofn  6592  f1ompt  6851  f1oresrab  6865  fsn  6873  fsnunf  6923  f1ocnvfv1  7010  f1ocnvfv2  7011  fsnex  7016  f1ocnvdm  7018  fcof1oinvd  7026  fveqf1o  7035  isocnv  7060  isocnv3  7062  isores2  7063  isotr  7066  isofr2  7074  isopolem  7075  isosolem  7077  f1oiso2  7082  weniso  7084  f1ofveu  7128  f1oexrnex  7610  f1oabexg  7620  wemoiso  7652  suppsnop  7822  smoiso  7977  mapsnd  8428  ralxpmap  8438  f1oen2g  8504  en1  8554  enfixsn  8604  mapen  8659  ac6sfi  8740  domunfican  8769  fiint  8773  mapfienlem1  8846  mapfienlem2  8847  mapfienlem3  8848  mapfien  8849  supisoex  8916  supiso  8917  ordiso2  8957  ordtypelem10  8969  unxpwdom2  9030  cantnfle  9112  cantnfp1lem3  9121  cantnflem1b  9127  cantnflem1d  9129  cantnflem1  9130  cnfcomlem  9140  cnfcom  9141  cnfcom2lem  9142  cnfcom2  9143  cnfcom3lem  9144  cnfcom3  9145  cnfcom3clem  9146  djuin  9325  infxpenlem  9417  infxpenc  9422  infxpenc2lem2  9424  fseqenlem1  9428  acndom  9455  acndom2  9458  infpwfien  9466  iunfictbso  9518  infmap2  9618  ackbij2lem2  9640  infpssrlem3  9705  infpssrlem4  9706  fin23lem30  9742  isf32lem6  9758  isf32lem7  9759  isf32lem8  9760  enfin1ai  9784  axcc3  9838  axcclem  9857  ttukeylem7  9915  fpwwe2lem6  10035  fpwwe2lem7  10036  fpwwe2lem9  10038  canthp1lem2  10053  canthp1  10054  pwfseqlem4a  10061  pwfseqlem5  10063  axdc4uzlem  13335  seqf1olem1  13394  seqf1olem2  13395  seqf1o  13396  hashkf  13677  hasheqf1oi  13697  hasheqf1od  13699  hashcl  13702  hashgadd  13723  hashfacen  13797  hashf1lem1  13798  fz1isolem  13804  seqcoll  13807  seqcoll2  13808  cnrecnv  14504  sumeq2ii  15030  summolem3  15051  summolem2a  15052  fsum  15057  fsumf1o  15060  fsumss  15062  fsumcl2lem  15068  fsumadd  15076  fsummulc2  15119  fsumrelem  15142  ackbijnn  15163  prodeq2ii  15247  prodmolem3  15267  prodmolem2a  15268  fprod  15275  fprodf1o  15280  fprodss  15282  fprodser  15283  fprodcl2lem  15284  fprodmul  15294  fproddiv  15295  fprodn0  15313  fproddvdsd  15664  sadcaddlem  15784  sadadd2lem  15786  sadadd3  15788  sadaddlem  15793  sadasslem  15797  sadeq  15799  phimullem  16094  eulerthlem1  16096  eulerthlem2  16097  unbenlem  16222  vdwlem8  16302  0ram  16334  wunndx  16483  xpsaddlem  16825  xpsvsca  16829  xpsle  16831  idfucl  17130  setccatid  17323  setcinv  17329  catcisolem  17345  estrccatid  17361  funcestrcsetclem7  17375  funcestrcsetclem8  17376  funcsetcestrclem7  17390  funcsetcestrclem8  17391  yonffthlem  17511  gsumpropd2lem  17868  idmhm  17944  mhmf1o  17945  gsumws1  17981  ielefmnd  18031  idghm  18352  ghmf1o  18367  permsetex  18477  symgbas  18478  elsymgbas  18481  symgbasf  18483  symgbasfi  18486  symg1bas  18498  symggrp  18507  lactghmga  18512  symgfixf1  18544  f1omvdmvd  18550  f1omvdconj  18553  f1omvdco2  18555  pmtrfconj  18573  symggen  18577  pmtrdifellem1  18583  pmtrdifellem2  18584  psgnunilem1  18600  gsumval3eu  19003  gsumval3lem1  19004  gsumval3  19006  gsumzf1o  19011  gsumconst  19033  gsumsub  19047  gsumcom2  19074  dprdfsub  19122  dprdf1o  19133  dprdsn  19137  ablfaclem2  19187  srngcl  19602  lmhmf1o  19794  fidomndrnglem  20055  psrass1lem  20133  psrnegcl  20152  psrlinv  20153  coe1f2  20353  coe1add  20408  evls1rhmlem  20460  evl1sca  20473  pf1ind  20494  gsumfsum  20588  zntoslem  20679  islinds2  20933  lindsmm  20948  mat1dimelbas  21056  mat1f  21067  mdetleib2  21173  mdetrsca  21188  mdetralt  21193  mdetunilem7  21203  mdetunilem9  21205  ssidcn  21839  hmphdis  22380  indishmph  22382  cmphaushmeo  22384  ordthmeolem  22385  txhmeo  22387  qtopf1  22400  ufldom  22546  symgtgp  22690  tsmsf1o  22729  iducn  22868  imasdsf1olem  22959  xpsdsval  22967  imasf1obl  23074  icchmeo  23525  iccpnfcnv  23528  xrhmeo  23530  cnheiborlem  23538  ovolctb  24073  ovoliunlem1  24085  ovoliunlem2  24086  iunmbl2  24140  dyadmbl  24183  vitalilem2  24192  vitalilem3  24193  vitalilem4  24194  vitalilem5  24195  mbfid  24218  dvid  24500  dvexp  24535  dvcnvlem  24558  dvcnv  24559  dvcnvrelem2  24600  dvcnvre  24601  efcvx  25023  reefgim  25024  efif1olem4  25116  eff1olem  25119  logrncl  25138  relogcl  25146  dvrelog  25207  relogcn  25208  logcn  25217  logf1o2  25220  dvlog  25221  dvlog2  25223  advlog  25224  advlogexp  25225  logtayl  25230  logccv  25233  dvcxp1  25308  loglesqrt  25326  asinrebnd  25466  dvatan  25500  efrlim  25534  amgmlem  25554  lgamcvg2  25619  wilthlem2  25633  wilthlem3  25634  sqff1o  25746  lgsqrlem4  25912  logdivsum  26096  log2sumbnd  26107  isismt  26307  motcl  26312  motco  26313  cnvmot  26314  motgrp  26316  motcgrg  26317  f1otrg  26644  f1otrge  26645  axlowdimlem10  26724  axcontlem5  26741  axcontlem10  26746  upgrres1  27082  umgrres1  27083  upgriseupth  27971  pliguhgr  28248  dmadjrn  29657  unopnorm  29679  unopadj  29681  unoplin  29682  counop  29683  idcnop  29743  idhmop  29744  unopbd  29777  bracnln  29871  cnvbraval  29872  leopnmid  29900  nmopleid  29901  hmopidmch  29915  hmopidmpj  29916  disjrdx  30328  fmptco1f1o  30365  isoun  30424  padct  30442  fcobij  30445  fcobijfs  30446  abliso  30691  symgfcoeu  30734  symgcom  30735  pmtrcnel  30741  pmtrcnel2  30742  pmtrcnelor  30743  cycpmco2f1  30774  cycpmco2rn  30775  cycpmco2lem2  30777  cycpmco2lem3  30778  cycpmco2lem4  30779  cycpmco2lem5  30780  cycpmco2lem6  30781  cycpmco2lem7  30782  cycpmco2  30783  cycpmconjv  30792  cycpmconjslem1  30804  cycpmconjslem2  30805  cycpmconjs  30806  islinds5  30940  ellspds  30941  tpr2rico  31163  xrge0iifmhm  31190  xrge0pluscn  31191  rrhre  31270  esumf1o  31317  volmeas  31498  eulerpartgbij  31638  eulerpartlemmf  31641  eulerpartlemgvv  31642  eulerpartlemgf  31645  eulerpartlemgs2  31646  eulerpartlemn  31647  ballotlemsima  31781  reprpmtf1o  31905  logdivsqrle  31929  hgt750lemg  31933  deranglem  32421  derangsn  32425  derangenlem  32426  subfacp1lem4  32438  subfacp1lem5  32439  subfacp1lem6  32440  cvmfolem  32534  cvmliftlem6  32545  poimirlem1  34934  poimirlem2  34935  poimirlem3  34936  poimirlem4  34937  poimirlem6  34939  poimirlem7  34940  poimirlem9  34942  poimirlem11  34944  poimirlem12  34945  poimirlem16  34949  poimirlem17  34950  poimirlem19  34952  poimirlem20  34953  poimirlem22  34955  poimirlem26  34959  poimirlem27  34960  poimirlem28  34961  poimirlem32  34965  mblfinlem2  34971  dvasin  35017  f1ocan1fv  35040  metf1o  35069  ismtyval  35114  isismty  35115  ismtyima  35117  ismtyhmeolem  35118  ismtybndlem  35120  ismrer1  35152  reheibor  35153  grposnOLD  35196  rngoisocnv  35295  lflnegl  36248  lautset  37254  islaut  37255  lautcl  37259  lautco  37269  pautsetN  37270  ispautN  37271  ldilco  37288  ltrncoidN  37300  ltrncoval  37317  trlcoabs2N  37894  trlcoat  37895  trlcone  37900  cdlemg47a  37906  cdlemg46  37907  cdlemg47  37908  trljco  37912  tgrpgrplem  37921  tendoidcl  37941  tendo0co2  37960  tendo0pl  37963  cdlemi2  37991  cdlemk2  38004  cdlemk4  38006  cdlemk8  38010  cdlemkid2  38096  cdlemk45  38119  cdlemk53b  38128  cdlemk53  38129  cdlemk55a  38131  erng1r  38167  tendocnv  38193  dvalveclem  38197  dva0g  38199  dvhgrp  38279  dvh0g  38283  dvhopN  38288  cdlemn3  38369  cdlemn8  38376  cdlemn9  38377  dihordlem7b  38387  dihopelvalcpre  38420  dihmeetlem1N  38462  dihglblem5apreN  38463  lcfrlem13  38727  hvmapclN  38936  hvmapcl2  38938  mapfzcons  39450  mzpresrename  39484  diophrw  39493  eldioph2  39496  diophren  39547  kelac1  39800  imasgim  39837  lnrfg  39856  brco2f1o  40517  brco3f1o  40518  clsneikex  40591  clsneinex  40592  clsneiel1  40593  neicvgmex  40602  neicvgel1  40604  dssmapntrcls  40613  stoweidlem27  42460  stoweidlem31  42464  stoweidlem39  42472  fourierdlem20  42560  fourierdlem50  42589  fourierdlem52  42591  fourierdlem54  42593  fourierdlem64  42603  fourierdlem76  42615  fourierdlem102  42641  fourierdlem114  42653  sge0f1o  42812  nnfoctbdjlem  42885  isomenndlem  42960  ovnsubaddlem1  43000  reuf1odnf  43454  reuf1od  43455  f1oresf1o2  43638  fundcmpsurbijinjpreimafv  43715  fundcmpsurinjimaid  43719  isomushgr  44136  isomuspgr  44144  isomgrtrlem  44148  1hegrlfgr  44152  mgmhmf1o  44199  idmgmhm  44200  funcringcsetcALTV2lem8  44459  funcringcsetclem8ALTV  44482  itcovalendof  44843  amgmwlem  45090
  Copyright terms: Public domain W3C validator