Theorem f1of 6362

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

Step	Hyp	Ref	Expression
1		f1of1 6361	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 6325	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 6106  –1-1→wf1 6107  –1-1-onto→wf1o 6109

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 198  df-an 385  df-f1 6115  df-f1o 6117

This theorem is referenced by:  f1ofn  6363  f1ompt  6612  f1oresrab  6626  fsn  6634  fsnunf  6685  f1ocnvfv1  6765  f1ocnvfv2  6766  fsnex  6771  f1ocnvdm  6773  fcof1oinvd  6781  fveqf1o  6790  isocnv  6813  isocnv3  6815  isores2  6816  isotr  6819  isofr2  6827  isopolem  6828  isosolem  6830  f1oiso2  6835  weniso  6837  f1ofveu  6878  f1oexrnex  7354  f1oabexg  7364  wemoiso  7392  suppsnop  7552  smoiso  7704  mapsnd  8143  ralxpmap  8153  f1oen2g  8218  en1  8268  enfixsn  8317  mapen  8372  ac6sfi  8452  domunfican  8481  fiint  8485  mapfienlem1  8558  mapfienlem2  8559  mapfienlem3  8560  mapfien  8561  supisoex  8628  supiso  8629  ordiso2  8668  ordtypelem10  8680  hartogslem1  8695  unxpwdom2  8741  cantnfle  8824  cantnfp1lem3  8833  cantnflem1b  8839  cantnflem1d  8841  cantnflem1  8842  cnfcomlem  8852  cnfcom  8853  cnfcom2lem  8854  cnfcom2  8855  cnfcom3lem  8856  cnfcom3  8857  cnfcom3clem  8858  djuin  9036  infxpenlem  9128  infxpenc  9133  infxpenc2lem2  9135  fseqenlem1  9139  acndom  9166  acndom2  9169  infpwfien  9177  iunfictbso  9229  infmap2  9334  ackbij2lem2  9356  infpssrlem3  9421  infpssrlem4  9422  fin23lem30  9458  isf32lem6  9474  isf32lem7  9475  isf32lem8  9476  enfin1ai  9500  axcc3  9554  axcclem  9573  ttukeylem7  9631  fpwwe2lem6  9751  fpwwe2lem7  9752  fpwwe2lem9  9754  canthp1lem2  9769  canthp1  9770  pwfseqlem4a  9777  pwfseqlem5  9779  dfle2  12215  axdc4uzlem  13025  seqf1olem1  13082  seqf1olem2  13083  seqf1o  13084  hashkf  13358  hasheqf1oi  13379  hasheqf1od  13381  hashcl  13384  hashgadd  13403  hashfacen  13474  hashf1lem1  13475  fz1isolem  13481  seqcoll  13484  seqcoll2  13485  cnrecnv  14147  sumeq2ii  14665  summolem3  14687  summolem2a  14688  fsum  14693  fsumf1o  14696  fsumss  14698  fsumcl2lem  14704  fsumadd  14712  fsummulc2  14757  fsumrelem  14780  ackbijnn  14801  prodeq2ii  14883  prodmolem3  14903  prodmolem2a  14904  fprod  14911  fprodf1o  14916  fprodss  14918  fprodser  14919  fprodcl2lem  14920  fprodmul  14930  fproddiv  14931  fprodn0  14949  fproddvdsd  15298  sadcaddlem  15417  sadadd2lem  15419  sadadd3  15421  sadaddlem  15426  sadasslem  15430  sadeq  15432  phimullem  15720  eulerthlem1  15722  eulerthlem2  15723  unbenlem  15848  vdwlem8  15928  0ram  15960  wunndx  16108  xpsaddlem  16459  xpsvsca  16463  xpsle  16465  idfucl  16764  setccatid  16957  setcinv  16963  catcisolem  16979  estrccatid  16995  funcestrcsetclem7  17010  funcestrcsetclem8  17011  funcsetcestrclem7  17025  funcsetcestrclem8  17026  yonffthlem  17146  gsumpropd2lem  17497  idmhm  17568  mhmf1o  17569  gsumws1  17600  idghm  17896  ghmf1o  17911  symgval  18019  symgbas  18020  elsymgbas  18022  symgbasf  18024  symgbasfi  18026  symg1bas  18036  symggrp  18040  symgid  18041  lactghmga  18044  symgfixf1  18077  f1omvdmvd  18083  f1omvdconj  18086  f1omvdco2  18088  pmtrfconj  18106  symggen  18110  pmtrdifellem1  18116  pmtrdifellem2  18117  psgnunilem1  18133  gsumval3eu  18525  gsumval3lem1  18526  gsumval3  18528  gsumzf1o  18533  gsumconst  18554  gsumsub  18568  gsumcom2  18594  dprdfsub  18641  dprdf1o  18652  dprdsn  18656  ablfaclem2  18706  srngcl  19078  lmhmf1o  19272  fidomndrnglem  19534  psrass1lem  19605  psrnegcl  19624  psrlinv  19625  coe1f2  19806  coe1add  19861  evls1rhmlem  19913  evl1sca  19925  pf1ind  19946  gsumfsum  20040  zntoslem  20131  islinds2  20382  lindsmm  20397  mat1dimelbas  20508  mat1f  20519  mdetleib2  20625  mdetrsca  20640  mdetralt  20645  mdetunilem7  20655  mdetunilem9  20657  ssidcn  21293  hausdiag  21682  hmphdis  21833  indishmph  21835  cmphaushmeo  21837  ordthmeolem  21838  txhmeo  21840  qtopf1  21853  ufldom  21999  symgtgp  22138  tsmsf1o  22181  iducn  22320  imasdsf1olem  22411  xpsdsval  22419  imasf1obl  22526  icchmeo  22973  iccpnfcnv  22976  xrhmeo  22978  cnheiborlem  22986  ovolctb  23493  ovoliunlem1  23505  ovoliunlem2  23506  iunmbl2  23560  dyadmbl  23603  vitalilem2  23612  vitalilem3  23613  vitalilem4  23614  vitalilem5  23615  mbfid  23638  dvid  23917  dvexp  23952  dvcnvlem  23975  dvcnv  23976  dvcnvrelem2  24017  dvcnvre  24018  efcvx  24439  reefgim  24440  efif1olem4  24528  eff1olem  24531  logrncl  24550  relogcl  24558  dvrelog  24619  relogcn  24620  logcn  24629  logf1o2  24632  dvlog  24633  dvlog2  24635  advlog  24636  advlogexp  24637  logtayl  24642  logccv  24645  dvcxp1  24717  loglesqrt  24735  asinrebnd  24864  dvatan  24898  efrlim  24932  amgmlem  24952  lgamcvg2  25017  wilthlem2  25031  wilthlem3  25032  sqff1o  25144  lgsqrlem4  25310  logdivsum  25458  log2sumbnd  25469  isismt  25665  motcl  25670  motco  25671  cnvmot  25672  motgrp  25674  motcgrg  25675  f1otrg  25987  f1otrge  25988  axlowdimlem10  26067  axcontlem5  26084  axcontlem10  26089  upgrres1  26443  umgrres1  26444  upgriseupth  27402  pliguhgr  27691  dmadjrn  29104  unopnorm  29126  unopadj  29128  unoplin  29129  counop  29130  idcnop  29190  idhmop  29191  unopbd  29224  bracnln  29318  cnvbraval  29319  leopnmid  29347  nmopleid  29348  hmopidmch  29362  hmopidmpj  29363  disjrdx  29751  fmptco1f1o  29783  isoun  29828  padct  29846  fcobij  29849  fcobijfs  29850  abliso  30043  symgfcoeu  30192  tpr2rico  30305  xrge0iifmhm  30332  xrge0pluscn  30333  rrhre  30412  esumf1o  30459  volmeas  30641  eulerpartgbij  30781  eulerpartlemmf  30784  eulerpartlemgvv  30785  eulerpartlemgf  30788  eulerpartlemgs2  30789  eulerpartlemn  30790  ballotlemsima  30924  reprpmtf1o  31051  logdivsqrle  31075  hgt750lemg  31079  deranglem  31492  derangsn  31496  derangenlem  31497  subfacp1lem4  31509  subfacp1lem5  31510  subfacp1lem6  31511  cvmfolem  31605  cvmliftlem6  31616  poimirlem1  33741  poimirlem2  33742  poimirlem3  33743  poimirlem4  33744  poimirlem6  33746  poimirlem7  33747  poimirlem9  33749  poimirlem11  33751  poimirlem12  33752  poimirlem16  33756  poimirlem17  33757  poimirlem19  33759  poimirlem20  33760  poimirlem22  33762  poimirlem26  33766  poimirlem27  33767  poimirlem28  33768  poimirlem32  33772  mblfinlem2  33778  dvasin  33826  f1ocan1fv  33851  metf1o  33880  ismtyval  33928  isismty  33929  ismtyima  33931  ismtyhmeolem  33932  ismtybndlem  33934  ismrer1  33966  reheibor  33967  grposnOLD  34010  rngoisocnv  34109  lflnegl  34874  lautset  35880  islaut  35881  lautcl  35885  lautco  35895  pautsetN  35896  ispautN  35897  ldilco  35914  ltrncoidN  35926  ltrncoval  35943  trlcoabs2N  36520  trlcoat  36521  trlcone  36526  cdlemg47a  36532  cdlemg46  36533  cdlemg47  36534  trljco  36538  tgrpgrplem  36547  tendoidcl  36567  tendo0co2  36586  tendo0pl  36589  cdlemi2  36617  cdlemk2  36630  cdlemk4  36632  cdlemk8  36636  cdlemkid2  36722  cdlemk45  36745  cdlemk53b  36754  cdlemk53  36755  cdlemk55a  36757  erng1r  36793  tendocnv  36819  dvalveclem  36823  dva0g  36825  dvhgrp  36905  dvh0g  36909  dvhopN  36914  cdlemn3  36995  cdlemn8  37002  cdlemn9  37003  dihordlem7b  37013  dihopelvalcpre  37046  dihmeetlem1N  37088  dihglblem5apreN  37089  lcfrlem13  37353  hvmapclN  37562  hvmapcl2  37564  mapfzcons  37798  mzpresrename  37832  diophrw  37841  eldioph2  37844  diophren  37896  kelac1  38151  imasgim  38188  lnrfg  38207  brco2f1o  38847  brco3f1o  38848  clsneikex  38921  clsneinex  38922  clsneiel1  38923  neicvgmex  38932  neicvgel1  38934  dssmapntrcls  38943  stoweidlem27  40740  stoweidlem31  40744  stoweidlem39  40752  fourierdlem20  40840  fourierdlem50  40869  fourierdlem52  40871  fourierdlem54  40873  fourierdlem64  40883  fourierdlem76  40895  fourierdlem102  40921  fourierdlem114  40933  sge0f1o  41095  nnfoctbdjlem  41168  isomenndlem  41243  ovnsubaddlem1  41283  f1oresf1o2  41898  1hegrlfgr  42298  mgmhmf1o  42372  idmgmhm  42373  funcringcsetcALTV2lem8  42628  funcringcsetclem8ALTV  42651  amgmwlem  43136