Theorem f1of 6137

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 6136	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 6101	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 5884  –1-1→wf1 5885  –1-1-onto→wf1o 5887

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 386  df-f1 5893  df-f1o 5895

This theorem is referenced by:  f1ofn  6138  f1ompt  6382  f1oresrab  6395  fsn  6402  fsnunf  6451  f1ocnvfv1  6532  f1ocnvfv2  6533  fsnex  6538  f1ocnvdm  6540  fcof1oinvd  6548  fveqf1o  6557  isocnv  6580  isocnv3  6582  isores2  6583  isotr  6586  isofr2  6594  isopolem  6595  isosolem  6597  f1oiso2  6602  weniso  6604  f1ofveu  6645  f1oexrnex  7115  f1oabexg  7125  wemoiso  7153  suppsnop  7309  smoiso  7459  mapsn  7899  ralxpmap  7907  f1oen2g  7972  en1  8023  enfixsn  8069  mapen  8124  ac6sfi  8204  domunfican  8233  fiint  8237  mapfienlem1  8310  mapfienlem2  8311  mapfienlem3  8312  mapfien  8313  supisoex  8380  supiso  8381  ordiso2  8420  ordtypelem10  8432  hartogslem1  8447  unxpwdom2  8493  cantnfle  8568  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1d  8585  cantnflem1  8586  cnfcomlem  8596  cnfcom  8597  cnfcom2lem  8598  cnfcom2  8599  cnfcom3lem  8600  cnfcom3  8601  cnfcom3clem  8602  infxpenlem  8836  infxpenc  8841  infxpenc2lem2  8843  fseqenlem1  8847  acndom  8874  acndom2  8877  infpwfien  8885  iunfictbso  8937  infmap2  9040  ackbij2lem2  9062  infpssrlem3  9127  infpssrlem4  9128  fin23lem30  9164  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  enfin1ai  9206  axcc3  9260  axcclem  9279  ttukeylem7  9337  fpwwe2lem6  9457  fpwwe2lem7  9458  fpwwe2lem9  9460  canthp1lem2  9475  canthp1  9476  pwfseqlem4a  9483  pwfseqlem5  9485  dfle2  11980  axdc4uzlem  12782  seqf1olem1  12840  seqf1olem2  12841  seqf1o  12842  hashkf  13119  hasheqf1oi  13140  hasheqf1oiOLD  13141  hasheqf1od  13144  hashcl  13147  hashgadd  13166  hashfacen  13238  hashf1lem1  13239  fz1isolem  13245  seqcoll  13248  seqcoll2  13249  cnrecnv  13905  sumeq2ii  14423  summolem3  14445  summolem2a  14446  fsum  14451  fsumf1o  14454  fsumss  14456  fsumcl2lem  14462  fsumadd  14470  fsummulc2  14516  fsumrelem  14539  ackbijnn  14560  prodeq2ii  14643  prodmolem3  14663  prodmolem2a  14664  fprod  14671  fprodf1o  14676  fprodss  14678  fprodser  14679  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodn0  14709  fproddvdsd  15059  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  sadeq  15194  phimullem  15484  eulerthlem1  15486  eulerthlem2  15487  unbenlem  15612  vdwlem8  15692  0ram  15724  wunndx  15878  xpsaddlem  16235  xpsvsca  16239  xpsle  16241  idfucl  16541  setccatid  16734  setcinv  16740  catcisolem  16756  estrccatid  16772  funcestrcsetclem7  16786  funcestrcsetclem8  16787  funcsetcestrclem7  16801  funcsetcestrclem8  16802  yonffthlem  16922  gsumpropd2lem  17273  idmhm  17344  mhmf1o  17345  gsumws1  17376  idghm  17675  ghmf1o  17690  symgval  17799  symgbas  17800  elsymgbas  17802  symgbasf  17804  symgbasfi  17806  symg1bas  17816  symggrp  17820  symgid  17821  lactghmga  17824  symgfixf1  17857  f1omvdmvd  17863  f1omvdconj  17866  f1omvdco2  17868  pmtrfconj  17886  symggen  17890  pmtrdifellem1  17896  pmtrdifellem2  17897  psgnunilem1  17913  gsumval3eu  18305  gsumval3lem1  18306  gsumval3  18308  gsumzf1o  18313  gsumconst  18334  gsumsub  18348  gsumcom2  18374  dprdfsub  18420  dprdf1o  18431  dprdsn  18435  ablfaclem2  18485  srngcl  18855  lmhmf1o  19046  fidomndrnglem  19306  psrass1lem  19377  psrnegcl  19396  psrlinv  19397  coe1f2  19579  coe1add  19634  evls1rhmlem  19686  evl1sca  19698  pf1ind  19719  gsumfsum  19813  zntoslem  19905  islinds2  20152  lindsmm  20167  mat1dimelbas  20277  mat1f  20288  mdetleib2  20394  mdetrsca  20409  mdetralt  20414  mdetunilem7  20424  mdetunilem9  20426  ssidcn  21059  hausdiag  21448  hmphdis  21599  indishmph  21601  cmphaushmeo  21603  ordthmeolem  21604  txhmeo  21606  qtopf1  21619  ufldom  21766  symgtgp  21905  tsmsf1o  21948  iducn  22087  imasdsf1olem  22178  xpsdsval  22186  imasf1obl  22293  icchmeo  22740  iccpnfcnv  22743  xrhmeo  22745  cnheiborlem  22753  ovolctb  23258  ovoliunlem1  23270  ovoliunlem2  23271  iunmbl2  23325  dyadmbl  23368  vitalilem2  23378  vitalilem3  23379  vitalilem4  23380  vitalilem5  23381  mbfid  23403  dvid  23681  dvexp  23716  dvcnvlem  23739  dvcnv  23740  dvcnvrelem2  23781  dvcnvre  23782  efcvx  24203  reefgim  24204  efif1olem4  24291  eff1olem  24294  logrncl  24314  relogcl  24322  dvrelog  24383  relogcn  24384  logcn  24393  logf1o2  24396  dvlog  24397  dvlog2  24399  advlog  24400  advlogexp  24401  logtayl  24406  logccv  24409  dvcxp1  24481  loglesqrt  24499  asinrebnd  24628  dvatan  24662  efrlim  24696  amgmlem  24716  lgamcvg2  24781  wilthlem2  24795  wilthlem3  24796  sqff1o  24908  lgsqrlem4  25074  logdivsum  25222  log2sumbnd  25233  isismt  25429  motcl  25434  motco  25435  cnvmot  25436  motgrp  25438  motcgrg  25439  f1otrg  25751  f1otrge  25752  axlowdimlem10  25831  axcontlem5  25848  axcontlem10  25853  upgrres1  26205  umgrres1  26206  upgriseupth  27067  pliguhgr  27338  dmadjrn  28754  unopnorm  28776  unopadj  28778  unoplin  28779  counop  28780  idcnop  28840  idhmop  28841  unopbd  28874  bracnln  28968  cnvbraval  28969  leopnmid  28997  nmopleid  28998  hmopidmch  29012  hmopidmpj  29013  disjrdx  29404  fmptco1f1o  29434  isoun  29479  padct  29497  fcobij  29500  fcobijfs  29501  abliso  29696  symgfcoeu  29845  tpr2rico  29958  xrge0iifmhm  29985  xrge0pluscn  29986  rrhre  30065  esumf1o  30112  volmeas  30294  eulerpartgbij  30434  eulerpartlemmf  30437  eulerpartlemgvv  30438  eulerpartlemgf  30441  eulerpartlemgs2  30442  eulerpartlemn  30443  ballotlemsima  30577  reprpmtf1o  30704  logdivsqrle  30728  hgt750lemg  30732  deranglem  31148  derangsn  31152  derangenlem  31153  subfacp1lem4  31165  subfacp1lem5  31166  subfacp1lem6  31167  cvmfolem  31261  cvmliftlem6  31272  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem32  33441  mblfinlem2  33447  dvasin  33496  f1ocan1fv  33521  metf1o  33551  ismtyval  33599  isismty  33600  ismtyima  33602  ismtyhmeolem  33603  ismtybndlem  33605  ismrer1  33637  reheibor  33638  grposnOLD  33681  rngoisocnv  33780  lflnegl  34363  lautset  35368  islaut  35369  lautcl  35373  lautco  35383  pautsetN  35384  ispautN  35385  ldilco  35402  ltrncoidN  35414  ltrncoval  35431  trlcoabs2N  36010  trlcoat  36011  trlcone  36016  cdlemg47a  36022  cdlemg46  36023  cdlemg47  36024  trljco  36028  tgrpgrplem  36037  tendoidcl  36057  tendo0co2  36076  tendo0pl  36079  cdlemi2  36107  cdlemk2  36120  cdlemk4  36122  cdlemk8  36126  cdlemkid2  36212  cdlemk45  36235  cdlemk53b  36244  cdlemk53  36245  cdlemk55a  36247  erng1r  36283  tendocnv  36310  dvalveclem  36314  dva0g  36316  dvhgrp  36396  dvh0g  36400  dvhopN  36405  cdlemn3  36486  cdlemn8  36493  cdlemn9  36494  dihordlem7b  36504  dihopelvalcpre  36537  dihmeetlem1N  36579  dihglblem5apreN  36580  lcfrlem13  36844  hvmapclN  37053  hvmapcl2  37055  mapfzcons  37279  mzpresrename  37313  diophrw  37322  eldioph2  37325  diophren  37377  kelac1  37633  imasgim  37670  lnrfg  37689  brco2f1o  38330  brco3f1o  38331  clsneikex  38404  clsneinex  38405  clsneiel1  38406  neicvgmex  38415  neicvgel1  38417  dssmapntrcls  38426  mapsnd  39388  stoweidlem27  40244  stoweidlem31  40248  stoweidlem39  40256  fourierdlem20  40344  fourierdlem50  40373  fourierdlem52  40375  fourierdlem54  40377  fourierdlem64  40387  fourierdlem76  40399  fourierdlem102  40425  fourierdlem114  40437  sge0f1o  40599  nnfoctbdjlem  40672  isomenndlem  40744  ovnsubaddlem1  40784  1hegrlfgr  41713  mgmhmf1o  41787  idmgmhm  41788  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  amgmwlem  42548