Theorem f1of 6617

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

Syntax hints:   → wi 4  ⟶wf 6353  –1-1→wf1 6354  –1-1-onto→wf1o 6356

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 209  df-an 399  df-f1 6362  df-f1o 6364

This theorem is referenced by:  f1ofn  6618  f1ompt  6877  f1oresrab  6891  fsn  6899  fsnunf  6949  f1ocnvfv1  7035  f1ocnvfv2  7036  fsnex  7041  f1ocnvdm  7043  fcof1oinvd  7051  fveqf1o  7060  isocnv  7085  isocnv3  7087  isores2  7088  isotr  7091  isofr2  7099  isopolem  7100  isosolem  7102  f1oiso2  7107  weniso  7109  f1ofveu  7153  f1oexrnex  7634  f1oabexg  7644  wemoiso  7676  suppsnop  7846  smoiso  8001  mapsnd  8452  ralxpmap  8462  f1oen2g  8528  en1  8578  enfixsn  8628  mapen  8683  ac6sfi  8764  domunfican  8793  fiint  8797  mapfienlem1  8870  mapfienlem2  8871  mapfienlem3  8872  mapfien  8873  supisoex  8940  supiso  8941  ordiso2  8981  ordtypelem10  8993  unxpwdom2  9054  cantnfle  9136  cantnfp1lem3  9145  cantnflem1b  9151  cantnflem1d  9153  cantnflem1  9154  cnfcomlem  9164  cnfcom  9165  cnfcom2lem  9166  cnfcom2  9167  cnfcom3lem  9168  cnfcom3  9169  cnfcom3clem  9170  djuin  9349  infxpenlem  9441  infxpenc  9446  infxpenc2lem2  9448  fseqenlem1  9452  acndom  9479  acndom2  9482  infpwfien  9490  iunfictbso  9542  infmap2  9642  ackbij2lem2  9664  infpssrlem3  9729  infpssrlem4  9730  fin23lem30  9766  isf32lem6  9782  isf32lem7  9783  isf32lem8  9784  enfin1ai  9808  axcc3  9862  axcclem  9881  ttukeylem7  9939  fpwwe2lem6  10059  fpwwe2lem7  10060  fpwwe2lem9  10062  canthp1lem2  10077  canthp1  10078  pwfseqlem4a  10085  pwfseqlem5  10087  axdc4uzlem  13354  seqf1olem1  13412  seqf1olem2  13413  seqf1o  13414  hashkf  13695  hasheqf1oi  13715  hasheqf1od  13717  hashcl  13720  hashgadd  13741  hashfacen  13815  hashf1lem1  13816  fz1isolem  13822  seqcoll  13825  seqcoll2  13826  cnrecnv  14526  sumeq2ii  15052  summolem3  15073  summolem2a  15074  fsum  15079  fsumf1o  15082  fsumss  15084  fsumcl2lem  15090  fsumadd  15098  fsummulc2  15141  fsumrelem  15164  ackbijnn  15185  prodeq2ii  15269  prodmolem3  15289  prodmolem2a  15290  fprod  15297  fprodf1o  15302  fprodss  15304  fprodser  15305  fprodcl2lem  15306  fprodmul  15316  fproddiv  15317  fprodn0  15335  fproddvdsd  15686  sadcaddlem  15808  sadadd2lem  15810  sadadd3  15812  sadaddlem  15817  sadasslem  15821  sadeq  15823  phimullem  16118  eulerthlem1  16120  eulerthlem2  16121  unbenlem  16246  vdwlem8  16326  0ram  16358  wunndx  16506  xpsaddlem  16848  xpsvsca  16852  xpsle  16854  idfucl  17153  setccatid  17346  setcinv  17352  catcisolem  17368  estrccatid  17384  funcestrcsetclem7  17398  funcestrcsetclem8  17399  funcsetcestrclem7  17413  funcsetcestrclem8  17414  yonffthlem  17534  gsumpropd2lem  17891  idmhm  17967  mhmf1o  17968  gsumws1  18004  ielefmnd  18054  idghm  18375  ghmf1o  18390  permsetex  18500  symgbas  18501  elsymgbas  18504  symgbasf  18506  symgbasfi  18509  symg1bas  18521  symggrp  18530  lactghmga  18535  symgfixf1  18567  f1omvdmvd  18573  f1omvdconj  18576  f1omvdco2  18578  pmtrfconj  18596  symggen  18600  pmtrdifellem1  18606  pmtrdifellem2  18607  psgnunilem1  18623  gsumval3eu  19026  gsumval3lem1  19027  gsumval3  19029  gsumzf1o  19034  gsumconst  19056  gsumsub  19070  gsumcom2  19097  dprdfsub  19145  dprdf1o  19156  dprdsn  19160  ablfaclem2  19210  srngcl  19628  lmhmf1o  19820  fidomndrnglem  20081  psrass1lem  20159  psrnegcl  20178  psrlinv  20179  coe1f2  20379  coe1add  20434  evls1rhmlem  20486  evl1sca  20499  pf1ind  20520  gsumfsum  20614  zntoslem  20705  islinds2  20959  lindsmm  20974  mat1dimelbas  21082  mat1f  21093  mdetleib2  21199  mdetrsca  21214  mdetralt  21219  mdetunilem7  21229  mdetunilem9  21231  ssidcn  21865  hmphdis  22406  indishmph  22408  cmphaushmeo  22410  ordthmeolem  22411  txhmeo  22413  qtopf1  22426  ufldom  22572  symgtgp  22716  tsmsf1o  22755  iducn  22894  imasdsf1olem  22985  xpsdsval  22993  imasf1obl  23100  icchmeo  23547  iccpnfcnv  23550  xrhmeo  23552  cnheiborlem  23560  ovolctb  24093  ovoliunlem1  24105  ovoliunlem2  24106  iunmbl2  24160  dyadmbl  24203  vitalilem2  24212  vitalilem3  24213  vitalilem4  24214  vitalilem5  24215  mbfid  24238  dvid  24517  dvexp  24552  dvcnvlem  24575  dvcnv  24576  dvcnvrelem2  24617  dvcnvre  24618  efcvx  25039  reefgim  25040  efif1olem4  25131  eff1olem  25134  logrncl  25153  relogcl  25161  dvrelog  25222  relogcn  25223  logcn  25232  logf1o2  25235  dvlog  25236  dvlog2  25238  advlog  25239  advlogexp  25240  logtayl  25245  logccv  25248  dvcxp1  25323  loglesqrt  25341  asinrebnd  25481  dvatan  25515  efrlim  25549  amgmlem  25569  lgamcvg2  25634  wilthlem2  25648  wilthlem3  25649  sqff1o  25761  lgsqrlem4  25927  logdivsum  26111  log2sumbnd  26122  isismt  26322  motcl  26327  motco  26328  cnvmot  26329  motgrp  26331  motcgrg  26332  f1otrg  26659  f1otrge  26660  axlowdimlem10  26739  axcontlem5  26756  axcontlem10  26761  upgrres1  27097  umgrres1  27098  upgriseupth  27988  pliguhgr  28265  dmadjrn  29674  unopnorm  29696  unopadj  29698  unoplin  29699  counop  29700  idcnop  29760  idhmop  29761  unopbd  29794  bracnln  29888  cnvbraval  29889  leopnmid  29917  nmopleid  29918  hmopidmch  29932  hmopidmpj  29933  disjrdx  30343  fmptco1f1o  30380  isoun  30439  padct  30457  fcobij  30460  fcobijfs  30461  abliso  30685  symgfcoeu  30728  symgcom  30729  pmtrcnel  30735  pmtrcnel2  30736  pmtrcnelor  30737  cycpmco2f1  30768  cycpmco2rn  30769  cycpmco2lem2  30771  cycpmco2lem3  30772  cycpmco2lem4  30773  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2lem7  30776  cycpmco2  30777  cycpmconjv  30786  cycpmconjslem1  30798  cycpmconjslem2  30799  cycpmconjs  30800  islinds5  30934  ellspds  30935  tpr2rico  31157  xrge0iifmhm  31184  xrge0pluscn  31185  rrhre  31264  esumf1o  31311  volmeas  31492  eulerpartgbij  31632  eulerpartlemmf  31635  eulerpartlemgvv  31636  eulerpartlemgf  31639  eulerpartlemgs2  31640  eulerpartlemn  31641  ballotlemsima  31775  reprpmtf1o  31899  logdivsqrle  31923  hgt750lemg  31927  deranglem  32415  derangsn  32419  derangenlem  32420  subfacp1lem4  32432  subfacp1lem5  32433  subfacp1lem6  32434  cvmfolem  32528  cvmliftlem6  32539  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem9  34903  poimirlem11  34905  poimirlem12  34906  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  poimirlem32  34926  mblfinlem2  34932  dvasin  34980  f1ocan1fv  35003  metf1o  35032  ismtyval  35080  isismty  35081  ismtyima  35083  ismtyhmeolem  35084  ismtybndlem  35086  ismrer1  35118  reheibor  35119  grposnOLD  35162  rngoisocnv  35261  lflnegl  36214  lautset  37220  islaut  37221  lautcl  37225  lautco  37235  pautsetN  37236  ispautN  37237  ldilco  37254  ltrncoidN  37266  ltrncoval  37283  trlcoabs2N  37860  trlcoat  37861  trlcone  37866  cdlemg47a  37872  cdlemg46  37873  cdlemg47  37874  trljco  37878  tgrpgrplem  37887  tendoidcl  37907  tendo0co2  37926  tendo0pl  37929  cdlemi2  37957  cdlemk2  37970  cdlemk4  37972  cdlemk8  37976  cdlemkid2  38062  cdlemk45  38085  cdlemk53b  38094  cdlemk53  38095  cdlemk55a  38097  erng1r  38133  tendocnv  38159  dvalveclem  38163  dva0g  38165  dvhgrp  38245  dvh0g  38249  dvhopN  38254  cdlemn3  38335  cdlemn8  38342  cdlemn9  38343  dihordlem7b  38353  dihopelvalcpre  38386  dihmeetlem1N  38428  dihglblem5apreN  38429  lcfrlem13  38693  hvmapclN  38902  hvmapcl2  38904  mapfzcons  39320  mzpresrename  39354  diophrw  39363  eldioph2  39366  diophren  39417  kelac1  39670  imasgim  39707  lnrfg  39726  brco2f1o  40389  brco3f1o  40390  clsneikex  40463  clsneinex  40464  clsneiel1  40465  neicvgmex  40474  neicvgel1  40476  dssmapntrcls  40485  stoweidlem27  42319  stoweidlem31  42323  stoweidlem39  42331  fourierdlem20  42419  fourierdlem50  42448  fourierdlem52  42450  fourierdlem54  42452  fourierdlem64  42462  fourierdlem76  42474  fourierdlem102  42500  fourierdlem114  42512  sge0f1o  42671  nnfoctbdjlem  42744  isomenndlem  42819  ovnsubaddlem1  42859  reuf1odnf  43313  reuf1od  43314  f1oresf1o2  43497  fundcmpsurbijinjpreimafv  43574  fundcmpsurinjimaid  43578  isomushgr  43998  isomuspgr  44006  isomgrtrlem  44010  1hegrlfgr  44014  mgmhmf1o  44061  idmgmhm  44062  funcringcsetcALTV2lem8  44321  funcringcsetclem8ALTV  44344  amgmwlem  44910