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

Theorem f1of 6609
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 6608 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 6569 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wf 6345  1-1wf1 6346  1-1-ontowf1o 6348
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 208  df-an 397  df-f1 6354  df-f1o 6356
This theorem is referenced by:  f1ofn  6610  f1ompt  6868  f1oresrab  6882  fsn  6890  fsnunf  6940  f1ocnvfv1  7024  f1ocnvfv2  7025  fsnex  7030  f1ocnvdm  7032  fcof1oinvd  7040  fveqf1o  7049  isocnv  7072  isocnv3  7074  isores2  7075  isotr  7078  isofr2  7086  isopolem  7087  isosolem  7089  f1oiso2  7094  weniso  7096  f1ofveu  7140  f1oexrnex  7620  f1oabexg  7630  wemoiso  7665  suppsnop  7835  smoiso  7990  mapsnd  8439  ralxpmap  8449  f1oen2g  8515  en1  8565  enfixsn  8615  mapen  8670  ac6sfi  8751  domunfican  8780  fiint  8784  mapfienlem1  8857  mapfienlem2  8858  mapfienlem3  8859  mapfien  8860  supisoex  8927  supiso  8928  ordiso2  8968  ordtypelem10  8980  unxpwdom2  9041  cantnfle  9123  cantnfp1lem3  9132  cantnflem1b  9138  cantnflem1d  9140  cantnflem1  9141  cnfcomlem  9151  cnfcom  9152  cnfcom2lem  9153  cnfcom2  9154  cnfcom3lem  9155  cnfcom3  9156  cnfcom3clem  9157  djuin  9336  infxpenlem  9428  infxpenc  9433  infxpenc2lem2  9435  fseqenlem1  9439  acndom  9466  acndom2  9469  infpwfien  9477  iunfictbso  9529  infmap2  9629  ackbij2lem2  9651  infpssrlem3  9716  infpssrlem4  9717  fin23lem30  9753  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  enfin1ai  9795  axcc3  9849  axcclem  9868  ttukeylem7  9926  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  canthp1lem2  10064  canthp1  10065  pwfseqlem4a  10072  pwfseqlem5  10074  axdc4uzlem  13341  seqf1olem1  13399  seqf1olem2  13400  seqf1o  13401  hashkf  13682  hasheqf1oi  13702  hasheqf1od  13704  hashcl  13707  hashgadd  13728  hashfacen  13802  hashf1lem1  13803  fz1isolem  13809  seqcoll  13812  seqcoll2  13813  cnrecnv  14514  sumeq2ii  15040  summolem3  15061  summolem2a  15062  fsum  15067  fsumf1o  15070  fsumss  15072  fsumcl2lem  15078  fsumadd  15086  fsummulc2  15129  fsumrelem  15152  ackbijnn  15173  prodeq2ii  15257  prodmolem3  15277  prodmolem2a  15278  fprod  15285  fprodf1o  15290  fprodss  15292  fprodser  15293  fprodcl2lem  15294  fprodmul  15304  fproddiv  15305  fprodn0  15323  fproddvdsd  15674  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  unbenlem  16234  vdwlem8  16314  0ram  16346  wunndx  16494  xpsaddlem  16836  xpsvsca  16840  xpsle  16842  idfucl  17141  setccatid  17334  setcinv  17340  catcisolem  17356  estrccatid  17372  funcestrcsetclem7  17386  funcestrcsetclem8  17387  funcsetcestrclem7  17401  funcsetcestrclem8  17402  yonffthlem  17522  gsumpropd2lem  17879  idmhm  17955  mhmf1o  17956  gsumws1  17992  idghm  18313  ghmf1o  18328  symgval  18437  symgbas  18438  elsymgbas  18440  symgbasf  18442  symgbasfi  18444  symg1bas  18455  symggrp  18460  symgid  18461  lactghmga  18464  symgfixf1  18496  f1omvdmvd  18502  f1omvdconj  18505  f1omvdco2  18507  pmtrfconj  18525  symggen  18529  pmtrdifellem1  18535  pmtrdifellem2  18536  psgnunilem1  18552  gsumval3eu  18955  gsumval3lem1  18956  gsumval3  18958  gsumzf1o  18963  gsumconst  18985  gsumsub  18999  gsumcom2  19026  dprdfsub  19074  dprdf1o  19085  dprdsn  19089  ablfaclem2  19139  srngcl  19557  lmhmf1o  19749  fidomndrnglem  20009  psrass1lem  20087  psrnegcl  20106  psrlinv  20107  coe1f2  20307  coe1add  20362  evls1rhmlem  20414  evl1sca  20427  pf1ind  20448  gsumfsum  20542  zntoslem  20633  islinds2  20887  lindsmm  20902  mat1dimelbas  21010  mat1f  21021  mdetleib2  21127  mdetrsca  21142  mdetralt  21147  mdetunilem7  21157  mdetunilem9  21159  ssidcn  21793  hmphdis  22334  indishmph  22336  cmphaushmeo  22338  ordthmeolem  22339  txhmeo  22341  qtopf1  22354  ufldom  22500  symgtgp  22639  tsmsf1o  22682  iducn  22821  imasdsf1olem  22912  xpsdsval  22920  imasf1obl  23027  icchmeo  23474  iccpnfcnv  23477  xrhmeo  23479  cnheiborlem  23487  ovolctb  24020  ovoliunlem1  24032  ovoliunlem2  24033  iunmbl2  24087  dyadmbl  24130  vitalilem2  24139  vitalilem3  24140  vitalilem4  24141  vitalilem5  24142  mbfid  24165  dvid  24444  dvexp  24479  dvcnvlem  24502  dvcnv  24503  dvcnvrelem2  24544  dvcnvre  24545  efcvx  24966  reefgim  24967  efif1olem4  25056  eff1olem  25059  logrncl  25078  relogcl  25086  dvrelog  25147  relogcn  25148  logcn  25157  logf1o2  25160  dvlog  25161  dvlog2  25163  advlog  25164  advlogexp  25165  logtayl  25170  logccv  25173  dvcxp1  25248  loglesqrt  25266  asinrebnd  25406  dvatan  25440  efrlim  25475  amgmlem  25495  lgamcvg2  25560  wilthlem2  25574  wilthlem3  25575  sqff1o  25687  lgsqrlem4  25853  logdivsum  26037  log2sumbnd  26048  isismt  26248  motcl  26253  motco  26254  cnvmot  26255  motgrp  26257  motcgrg  26258  f1otrg  26585  f1otrge  26586  axlowdimlem10  26665  axcontlem5  26682  axcontlem10  26687  upgrres1  27023  umgrres1  27024  upgriseupth  27914  pliguhgr  28191  dmadjrn  29600  unopnorm  29622  unopadj  29624  unoplin  29625  counop  29626  idcnop  29686  idhmop  29687  unopbd  29720  bracnln  29814  cnvbraval  29815  leopnmid  29843  nmopleid  29844  hmopidmch  29858  hmopidmpj  29859  disjrdx  30270  fmptco1f1o  30307  isoun  30364  padct  30382  fcobij  30385  fcobijfs  30386  abliso  30611  symgfcoeu  30654  symgcom  30655  pmtrcnel  30661  pmtrcnel2  30662  pmtrcnelor  30663  cycpmco2f1  30694  cycpmco2rn  30695  cycpmco2lem2  30697  cycpmco2lem3  30698  cycpmco2lem4  30699  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2lem7  30702  cycpmco2  30703  cycpmconjv  30712  cycpmconjslem1  30724  cycpmconjslem2  30725  cycpmconjs  30726  islinds5  30860  ellspds  30861  tpr2rico  31055  xrge0iifmhm  31082  xrge0pluscn  31083  rrhre  31162  esumf1o  31209  volmeas  31390  eulerpartgbij  31530  eulerpartlemmf  31533  eulerpartlemgvv  31534  eulerpartlemgf  31537  eulerpartlemgs2  31538  eulerpartlemn  31539  ballotlemsima  31673  reprpmtf1o  31797  logdivsqrle  31821  hgt750lemg  31825  deranglem  32311  derangsn  32315  derangenlem  32316  subfacp1lem4  32328  subfacp1lem5  32329  subfacp1lem6  32330  cvmfolem  32424  cvmliftlem6  32435  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem6  34780  poimirlem7  34781  poimirlem9  34783  poimirlem11  34785  poimirlem12  34786  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem22  34796  poimirlem26  34800  poimirlem27  34801  poimirlem28  34802  poimirlem32  34806  mblfinlem2  34812  dvasin  34860  f1ocan1fv  34884  metf1o  34913  ismtyval  34961  isismty  34962  ismtyima  34964  ismtyhmeolem  34965  ismtybndlem  34967  ismrer1  34999  reheibor  35000  grposnOLD  35043  rngoisocnv  35142  lflnegl  36094  lautset  37100  islaut  37101  lautcl  37105  lautco  37115  pautsetN  37116  ispautN  37117  ldilco  37134  ltrncoidN  37146  ltrncoval  37163  trlcoabs2N  37740  trlcoat  37741  trlcone  37746  cdlemg47a  37752  cdlemg46  37753  cdlemg47  37754  trljco  37758  tgrpgrplem  37767  tendoidcl  37787  tendo0co2  37806  tendo0pl  37809  cdlemi2  37837  cdlemk2  37850  cdlemk4  37852  cdlemk8  37856  cdlemkid2  37942  cdlemk45  37965  cdlemk53b  37974  cdlemk53  37975  cdlemk55a  37977  erng1r  38013  tendocnv  38039  dvalveclem  38043  dva0g  38045  dvhgrp  38125  dvh0g  38129  dvhopN  38134  cdlemn3  38215  cdlemn8  38222  cdlemn9  38223  dihordlem7b  38233  dihopelvalcpre  38266  dihmeetlem1N  38308  dihglblem5apreN  38309  lcfrlem13  38573  hvmapclN  38782  hvmapcl2  38784  mapfzcons  39193  mzpresrename  39227  diophrw  39236  eldioph2  39239  diophren  39290  kelac1  39543  imasgim  39580  lnrfg  39599  brco2f1o  40262  brco3f1o  40263  clsneikex  40336  clsneinex  40337  clsneiel1  40338  neicvgmex  40347  neicvgel1  40349  dssmapntrcls  40358  stoweidlem27  42193  stoweidlem31  42197  stoweidlem39  42205  fourierdlem20  42293  fourierdlem50  42322  fourierdlem52  42324  fourierdlem54  42326  fourierdlem64  42336  fourierdlem76  42348  fourierdlem102  42374  fourierdlem114  42386  sge0f1o  42545  nnfoctbdjlem  42618  isomenndlem  42693  ovnsubaddlem1  42733  reuf1odnf  43187  reuf1od  43188  f1oresf1o2  43371  isomushgr  43838  isomuspgr  43846  isomgrtrlem  43850  1hegrlfgr  43854  mgmhmf1o  43901  idmgmhm  43902  ielefmnd  43954  symgsubmefmndALT  43966  funcringcsetcALTV2lem8  44212  funcringcsetclem8ALTV  44235  amgmwlem  44801
  Copyright terms: Public domain W3C validator