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

Theorem f1of 6175
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 6174 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
2 f1f 6139 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
31, 2syl 17 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wf 5922  1-1wf1 5923  1-1-ontowf1o 5925
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 197  df-an 385  df-f1 5931  df-f1o 5933
This theorem is referenced by:  f1ofn  6176  f1ompt  6422  f1oresrab  6435  fsn  6442  fsnunf  6492  f1ocnvfv1  6572  f1ocnvfv2  6573  fsnex  6578  f1ocnvdm  6580  fcof1oinvd  6588  fveqf1o  6597  isocnv  6620  isocnv3  6622  isores2  6623  isotr  6626  isofr2  6634  isopolem  6635  isosolem  6637  f1oiso2  6642  weniso  6644  f1ofveu  6685  f1oexrnex  7157  f1oabexg  7167  wemoiso  7195  suppsnop  7354  smoiso  7504  mapsn  7941  ralxpmap  7949  f1oen2g  8014  en1  8064  enfixsn  8110  mapen  8165  ac6sfi  8245  domunfican  8274  fiint  8278  mapfienlem1  8351  mapfienlem2  8352  mapfienlem3  8353  mapfien  8354  supisoex  8421  supiso  8422  ordiso2  8461  ordtypelem10  8473  hartogslem1  8488  unxpwdom2  8534  cantnfle  8606  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1d  8623  cantnflem1  8624  cnfcomlem  8634  cnfcom  8635  cnfcom2lem  8636  cnfcom2  8637  cnfcom3lem  8638  cnfcom3  8639  cnfcom3clem  8640  infxpenlem  8874  infxpenc  8879  infxpenc2lem2  8881  fseqenlem1  8885  acndom  8912  acndom2  8915  infpwfien  8923  iunfictbso  8975  infmap2  9078  ackbij2lem2  9100  infpssrlem3  9165  infpssrlem4  9166  fin23lem30  9202  isf32lem6  9218  isf32lem7  9219  isf32lem8  9220  enfin1ai  9244  axcc3  9298  axcclem  9317  ttukeylem7  9375  fpwwe2lem6  9495  fpwwe2lem7  9496  fpwwe2lem9  9498  canthp1lem2  9513  canthp1  9514  pwfseqlem4a  9521  pwfseqlem5  9523  dfle2  12018  axdc4uzlem  12822  seqf1olem1  12880  seqf1olem2  12881  seqf1o  12882  hashkf  13159  hasheqf1oi  13180  hasheqf1od  13182  hashcl  13185  hashgadd  13204  hashfacen  13276  hashf1lem1  13277  fz1isolem  13283  seqcoll  13286  seqcoll2  13287  cnrecnv  13949  sumeq2ii  14467  summolem3  14489  summolem2a  14490  fsum  14495  fsumf1o  14498  fsumss  14500  fsumcl2lem  14506  fsumadd  14514  fsummulc2  14560  fsumrelem  14583  ackbijnn  14604  prodeq2ii  14687  prodmolem3  14707  prodmolem2a  14708  fprod  14715  fprodf1o  14720  fprodss  14722  fprodser  14723  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodn0  14753  fproddvdsd  15106  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadaddlem  15235  sadasslem  15239  sadeq  15241  phimullem  15531  eulerthlem1  15533  eulerthlem2  15534  unbenlem  15659  vdwlem8  15739  0ram  15771  wunndx  15925  xpsaddlem  16282  xpsvsca  16286  xpsle  16288  idfucl  16588  setccatid  16781  setcinv  16787  catcisolem  16803  estrccatid  16819  funcestrcsetclem7  16833  funcestrcsetclem8  16834  funcsetcestrclem7  16848  funcsetcestrclem8  16849  yonffthlem  16969  gsumpropd2lem  17320  idmhm  17391  mhmf1o  17392  gsumws1  17423  idghm  17722  ghmf1o  17737  symgval  17845  symgbas  17846  elsymgbas  17848  symgbasf  17850  symgbasfi  17852  symg1bas  17862  symggrp  17866  symgid  17867  lactghmga  17870  symgfixf1  17903  f1omvdmvd  17909  f1omvdconj  17912  f1omvdco2  17914  pmtrfconj  17932  symggen  17936  pmtrdifellem1  17942  pmtrdifellem2  17943  psgnunilem1  17959  gsumval3eu  18351  gsumval3lem1  18352  gsumval3  18354  gsumzf1o  18359  gsumconst  18380  gsumsub  18394  gsumcom2  18420  dprdfsub  18466  dprdf1o  18477  dprdsn  18481  ablfaclem2  18531  srngcl  18903  lmhmf1o  19094  fidomndrnglem  19354  psrass1lem  19425  psrnegcl  19444  psrlinv  19445  coe1f2  19627  coe1add  19682  evls1rhmlem  19734  evl1sca  19746  pf1ind  19767  gsumfsum  19861  zntoslem  19953  islinds2  20200  lindsmm  20215  mat1dimelbas  20325  mat1f  20336  mdetleib2  20442  mdetrsca  20457  mdetralt  20462  mdetunilem7  20472  mdetunilem9  20474  ssidcn  21107  hausdiag  21496  hmphdis  21647  indishmph  21649  cmphaushmeo  21651  ordthmeolem  21652  txhmeo  21654  qtopf1  21667  ufldom  21813  symgtgp  21952  tsmsf1o  21995  iducn  22134  imasdsf1olem  22225  xpsdsval  22233  imasf1obl  22340  icchmeo  22787  iccpnfcnv  22790  xrhmeo  22792  cnheiborlem  22800  ovolctb  23304  ovoliunlem1  23316  ovoliunlem2  23317  iunmbl2  23371  dyadmbl  23414  vitalilem2  23423  vitalilem3  23424  vitalilem4  23425  vitalilem5  23426  mbfid  23448  dvid  23726  dvexp  23761  dvcnvlem  23784  dvcnv  23785  dvcnvrelem2  23826  dvcnvre  23827  efcvx  24248  reefgim  24249  efif1olem4  24336  eff1olem  24339  logrncl  24359  relogcl  24367  dvrelog  24428  relogcn  24429  logcn  24438  logf1o2  24441  dvlog  24442  dvlog2  24444  advlog  24445  advlogexp  24446  logtayl  24451  logccv  24454  dvcxp1  24526  loglesqrt  24544  asinrebnd  24673  dvatan  24707  efrlim  24741  amgmlem  24761  lgamcvg2  24826  wilthlem2  24840  wilthlem3  24841  sqff1o  24953  lgsqrlem4  25119  logdivsum  25267  log2sumbnd  25278  isismt  25474  motcl  25479  motco  25480  cnvmot  25481  motgrp  25483  motcgrg  25484  f1otrg  25796  f1otrge  25797  axlowdimlem10  25876  axcontlem5  25893  axcontlem10  25898  upgrres1  26250  umgrres1  26251  upgriseupth  27185  pliguhgr  27468  dmadjrn  28882  unopnorm  28904  unopadj  28906  unoplin  28907  counop  28908  idcnop  28968  idhmop  28969  unopbd  29002  bracnln  29096  cnvbraval  29097  leopnmid  29125  nmopleid  29126  hmopidmch  29140  hmopidmpj  29141  disjrdx  29530  fmptco1f1o  29562  isoun  29607  padct  29625  fcobij  29628  fcobijfs  29629  abliso  29824  symgfcoeu  29973  tpr2rico  30086  xrge0iifmhm  30113  xrge0pluscn  30114  rrhre  30193  esumf1o  30240  volmeas  30422  eulerpartgbij  30562  eulerpartlemmf  30565  eulerpartlemgvv  30566  eulerpartlemgf  30569  eulerpartlemgs2  30570  eulerpartlemn  30571  ballotlemsima  30705  reprpmtf1o  30832  logdivsqrle  30856  hgt750lemg  30860  deranglem  31274  derangsn  31278  derangenlem  31279  subfacp1lem4  31291  subfacp1lem5  31292  subfacp1lem6  31293  cvmfolem  31387  cvmliftlem6  31398  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem9  33548  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem32  33571  mblfinlem2  33577  dvasin  33626  f1ocan1fv  33651  metf1o  33681  ismtyval  33729  isismty  33730  ismtyima  33732  ismtyhmeolem  33733  ismtybndlem  33735  ismrer1  33767  reheibor  33768  grposnOLD  33811  rngoisocnv  33910  lflnegl  34681  lautset  35686  islaut  35687  lautcl  35691  lautco  35701  pautsetN  35702  ispautN  35703  ldilco  35720  ltrncoidN  35732  ltrncoval  35749  trlcoabs2N  36327  trlcoat  36328  trlcone  36333  cdlemg47a  36339  cdlemg46  36340  cdlemg47  36341  trljco  36345  tgrpgrplem  36354  tendoidcl  36374  tendo0co2  36393  tendo0pl  36396  cdlemi2  36424  cdlemk2  36437  cdlemk4  36439  cdlemk8  36443  cdlemkid2  36529  cdlemk45  36552  cdlemk53b  36561  cdlemk53  36562  cdlemk55a  36564  erng1r  36600  tendocnv  36627  dvalveclem  36631  dva0g  36633  dvhgrp  36713  dvh0g  36717  dvhopN  36722  cdlemn3  36803  cdlemn8  36810  cdlemn9  36811  dihordlem7b  36821  dihopelvalcpre  36854  dihmeetlem1N  36896  dihglblem5apreN  36897  lcfrlem13  37161  hvmapclN  37370  hvmapcl2  37372  mapfzcons  37596  mzpresrename  37630  diophrw  37639  eldioph2  37642  diophren  37694  kelac1  37950  imasgim  37987  lnrfg  38006  brco2f1o  38647  brco3f1o  38648  clsneikex  38721  clsneinex  38722  clsneiel1  38723  neicvgmex  38732  neicvgel1  38734  dssmapntrcls  38743  mapsnd  39702  stoweidlem27  40562  stoweidlem31  40566  stoweidlem39  40574  fourierdlem20  40662  fourierdlem50  40691  fourierdlem52  40693  fourierdlem54  40695  fourierdlem64  40705  fourierdlem76  40717  fourierdlem102  40743  fourierdlem114  40755  sge0f1o  40917  nnfoctbdjlem  40990  isomenndlem  41065  ovnsubaddlem1  41105  1hegrlfgr  42038  mgmhmf1o  42112  idmgmhm  42113  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391  amgmwlem  42876
  Copyright terms: Public domain W3C validator