Theorem f1of 6700

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

Syntax hints:   → wi 4  ⟶wf 6414  –1-1→wf1 6415  –1-1-onto→wf1o 6417

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 206  df-an 396  df-f1 6423  df-f1o 6425

This theorem is referenced by:  f1ofn  6701  f1ompt  6967  f1oresrab  6981  fsn  6989  fsnunf  7039  f1ocnvfv1  7129  f1ocnvfv2  7130  fsnex  7135  f1ocnvdm  7137  fcof1oinvd  7145  fveqf1o  7155  isocnv  7181  isocnv3  7183  isores2  7184  isotr  7187  isofr2  7195  isopolem  7196  isosolem  7198  f1oiso2  7203  weniso  7205  f1ofveu  7250  f1oexrnex  7748  f1oabexg  7757  wemoiso  7789  suppsnop  7965  smoiso  8164  mapsnd  8632  ralxpmap  8642  f1oen2g  8711  en1  8765  en1OLD  8766  enfixsn  8821  mapen  8877  ac6sfi  8988  domunfican  9017  fiint  9021  mapfienlem1  9094  mapfienlem2  9095  mapfienlem3  9096  mapfien  9097  supisoex  9163  supiso  9164  ordiso2  9204  unxpwdom2  9277  cantnfle  9359  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1d  9376  cantnflem1  9377  cnfcomlem  9387  cnfcom  9388  cnfcom2lem  9389  cnfcom2  9390  cnfcom3lem  9391  cnfcom3  9392  cnfcom3clem  9393  djuin  9607  infxpenlem  9700  infxpenc  9705  infxpenc2lem2  9707  fseqenlem1  9711  acndom  9738  acndom2  9741  infpwfien  9749  iunfictbso  9801  infmap2  9905  ackbij2lem2  9927  infpssrlem3  9992  infpssrlem4  9993  fin23lem30  10029  isf32lem6  10045  isf32lem7  10046  isf32lem8  10047  enfin1ai  10071  axcc3  10125  axcclem  10144  ttukeylem7  10202  fpwwe2lem5  10322  fpwwe2lem6  10323  fpwwe2lem8  10325  canthp1lem2  10340  canthp1  10341  pwfseqlem4a  10348  pwfseqlem5  10350  axdc4uzlem  13631  seqf1olem1  13690  seqf1olem2  13691  seqf1o  13692  hashkf  13974  hasheqf1oi  13994  hasheqf1od  13996  hashcl  13999  hashgadd  14020  hashfacen  14094  hashfacenOLD  14095  hashf1lem1  14096  hashf1lem1OLD  14097  fz1isolem  14103  seqcoll  14106  seqcoll2  14107  cnrecnv  14804  sumeq2ii  15333  summolem3  15354  summolem2a  15355  fsum  15360  fsumf1o  15363  fsumss  15365  fsumcl2lem  15371  fsumadd  15380  fsummulc2  15424  fsumrelem  15447  ackbijnn  15468  prodeq2ii  15551  prodmolem3  15571  prodmolem2a  15572  fprod  15579  fprodf1o  15584  fprodss  15586  fprodser  15587  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodn0  15617  fproddvdsd  15972  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  sadasslem  16105  sadeq  16107  phimullem  16408  eulerthlem1  16410  eulerthlem2  16411  unbenlem  16537  vdwlem8  16617  0ram  16649  wunndx  16824  xpsaddlem  17201  xpsvsca  17205  xpsle  17207  idfucl  17512  setccatid  17715  setcinv  17721  catcisolem  17741  estrccatid  17764  funcestrcsetclem7  17779  funcestrcsetclem8  17780  funcsetcestrclem7  17794  funcsetcestrclem8  17795  yonffthlem  17916  gsumpropd2lem  18278  idmhm  18354  mhmf1o  18355  gsumws1  18391  ielefmnd  18441  idghm  18764  ghmf1o  18779  permsetexOLD  18892  symgbas  18893  elsymgbas  18896  symgbasf  18898  symgbasfi  18901  symg1bas  18913  symggrp  18923  lactghmga  18928  symgfixf1  18960  f1omvdmvd  18966  f1omvdconj  18969  f1omvdco2  18971  pmtrfconj  18989  symggen  18993  pmtrdifellem1  18999  pmtrdifellem2  19000  psgnunilem1  19016  gsumval3eu  19420  gsumval3lem1  19421  gsumval3  19423  gsumzf1o  19428  gsumconst  19450  gsumsub  19464  gsumcom2  19491  dprdfsub  19539  dprdf1o  19550  dprdsn  19554  ablfaclem2  19604  srngcl  20030  lmhmf1o  20223  fidomndrnglem  20491  gsumfsum  20577  zntoslem  20676  islinds2  20930  lindsmm  20945  psrass1lemOLD  21053  psrass1lem  21056  psrnegcl  21075  psrlinv  21076  coe1f2  21290  coe1add  21345  evls1rhmlem  21397  evl1sca  21410  pf1ind  21431  mat1dimelbas  21528  mat1f  21539  mdetleib2  21645  mdetrsca  21660  mdetralt  21665  mdetunilem7  21675  mdetunilem9  21677  ssidcn  22314  hmphdis  22855  indishmph  22857  cmphaushmeo  22859  ordthmeolem  22860  txhmeo  22862  qtopf1  22875  ufldom  23021  symgtgp  23165  tsmsf1o  23204  iducn  23343  imasdsf1olem  23434  xpsdsval  23442  imasf1obl  23550  icchmeo  24010  iccpnfcnv  24013  xrhmeo  24015  cnheiborlem  24023  ovolctb  24559  ovoliunlem1  24571  ovoliunlem2  24572  iunmbl2  24626  dyadmbl  24669  vitalilem2  24678  vitalilem3  24679  vitalilem4  24680  vitalilem5  24681  mbfid  24704  dvid  24987  dvexp  25022  dvcnvlem  25045  dvcnv  25046  dvcnvrelem2  25087  dvcnvre  25088  efcvx  25513  reefgim  25514  efif1olem4  25606  eff1olem  25609  logrncl  25628  relogcl  25636  dvrelog  25697  relogcn  25698  logcn  25707  logf1o2  25710  dvlog  25711  dvlog2  25713  advlog  25714  advlogexp  25715  logtayl  25720  logccv  25723  dvcxp1  25798  loglesqrt  25816  asinrebnd  25956  dvatan  25990  efrlim  26024  amgmlem  26044  lgamcvg2  26109  wilthlem2  26123  wilthlem3  26124  sqff1o  26236  lgsqrlem4  26402  logdivsum  26586  log2sumbnd  26597  isismt  26799  motcl  26804  motco  26805  cnvmot  26806  motgrp  26808  motcgrg  26809  f1otrg  27136  f1otrge  27137  axlowdimlem10  27222  axcontlem5  27239  axcontlem10  27244  upgrres1  27583  umgrres1  27584  upgriseupth  28472  pliguhgr  28749  dmadjrn  30158  unopnorm  30180  unopadj  30182  unoplin  30183  counop  30184  idcnop  30244  idhmop  30245  unopbd  30278  bracnln  30372  cnvbraval  30373  leopnmid  30401  nmopleid  30402  hmopidmch  30416  hmopidmpj  30417  disjrdx  30831  fmptco1f1o  30869  isoun  30936  padct  30956  fcobij  30959  fcobijfs  30960  abliso  31207  symgfcoeu  31253  symgcom  31254  pmtrcnel  31260  pmtrcnel2  31261  pmtrcnelor  31262  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem2  31296  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  cycpmconjv  31311  cycpmconjslem1  31323  cycpmconjslem2  31324  cycpmconjs  31325  islinds5  31465  ellspds  31466  tpr2rico  31764  xrge0iifmhm  31791  xrge0pluscn  31792  rrhre  31871  esumf1o  31918  volmeas  32099  eulerpartgbij  32239  eulerpartlemmf  32242  eulerpartlemgvv  32243  eulerpartlemgf  32246  eulerpartlemgs2  32247  eulerpartlemn  32248  ballotlemsima  32382  reprpmtf1o  32506  logdivsqrle  32530  hgt750lemg  32534  deranglem  33028  derangsn  33032  derangenlem  33033  subfacp1lem4  33045  subfacp1lem5  33046  subfacp1lem6  33047  cvmfolem  33141  cvmliftlem6  33152  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem32  35736  mblfinlem2  35742  dvasin  35788  f1ocan1fv  35811  metf1o  35840  ismtyval  35885  isismty  35886  ismtyima  35888  ismtyhmeolem  35889  ismtybndlem  35891  ismrer1  35923  reheibor  35924  grposnOLD  35967  rngoisocnv  36066  lflnegl  37017  lautset  38023  islaut  38024  lautcl  38028  lautco  38038  pautsetN  38039  ispautN  38040  ldilco  38057  ltrncoidN  38069  ltrncoval  38086  trlcoabs2N  38663  trlcoat  38664  trlcone  38669  cdlemg47a  38675  cdlemg46  38676  cdlemg47  38677  trljco  38681  tgrpgrplem  38690  tendoidcl  38710  tendo0co2  38729  tendo0pl  38732  cdlemi2  38760  cdlemk2  38773  cdlemk4  38775  cdlemk8  38779  cdlemkid2  38865  cdlemk45  38888  cdlemk53b  38897  cdlemk53  38898  cdlemk55a  38900  erng1r  38936  tendocnv  38962  dvalveclem  38966  dva0g  38968  dvhgrp  39048  dvh0g  39052  dvhopN  39057  cdlemn3  39138  cdlemn8  39145  cdlemn9  39146  dihordlem7b  39156  dihopelvalcpre  39189  dihmeetlem1N  39231  dihglblem5apreN  39232  lcfrlem13  39496  hvmapclN  39705  hvmapcl2  39707  dvrelog2  40000  dvrelog3  40001  sticksstones3  40032  sticksstones17  40047  sticksstones18  40048  sticksstones19  40049  metakunt33  40085  mapfzcons  40454  mzpresrename  40488  diophrw  40497  eldioph2  40500  diophren  40551  kelac1  40804  imasgim  40841  lnrfg  40860  brco2f1o  41531  brco3f1o  41532  clsneikex  41605  clsneinex  41606  clsneiel1  41607  neicvgmex  41616  neicvgel1  41618  dssmapntrcls  41627  stoweidlem27  43458  stoweidlem31  43462  stoweidlem39  43470  fourierdlem20  43558  fourierdlem50  43587  fourierdlem52  43589  fourierdlem54  43591  fourierdlem64  43601  fourierdlem76  43613  fourierdlem102  43639  fourierdlem114  43651  sge0f1o  43810  nnfoctbdjlem  43883  isomenndlem  43958  ovnsubaddlem1  43998  reuf1odnf  44486  reuf1od  44487  f1oresf1o2  44670  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjimaid  44751  isomushgr  45166  isomuspgr  45174  isomgrtrlem  45178  1hegrlfgr  45182  mgmhmf1o  45229  idmgmhm  45230  funcringcsetcALTV2lem8  45489  funcringcsetclem8ALTV  45512  itcovalendof  45903  thincciso  46218  amgmwlem  46392