Theorem f1of 6774

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

Syntax hints:   → wi 4  ⟶wf 6488  –1-1→wf1 6489  –1-1-onto→wf1o 6491

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 208  df-an 397  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1ofn  6775  f1ompt  7059  f1oresrab  7076  fsn  7084  fsnunf  7136  f1ounsn  7223  f1ocnvfv1  7227  f1ocnvfv2  7228  fsnex  7234  f1ocnvdm  7236  fcof1oinvd  7244  fveqf1o  7253  isocnv  7281  isocnv3  7283  isores2  7284  isotr  7287  isofr2  7295  isopolem  7296  isosolem  7298  f1oiso2  7303  weniso  7305  f1ofveu  7357  f1oexrnex  7874  f1oabexg  7889  f1oabexgOLD  7890  wemoiso  7922  mptcnfimad  7935  suppsnop  8125  smoiso  8299  mapsnd  8831  ralxpmap  8841  f1oen2g  8912  en1  8968  enfixsn  9021  mapen  9076  ac6sfi  9191  domunfican  9229  fiint  9234  mapfienlem1  9315  mapfienlem2  9316  mapfienlem3  9317  mapfien  9318  supisoex  9385  supiso  9386  ordiso2  9427  unxpwdom2  9500  cantnfle  9590  cantnfp1lem3  9599  cantnflem1b  9605  cantnflem1d  9607  cantnflem1  9608  cnfcomlem  9618  cnfcom  9619  cnfcom2lem  9620  cnfcom2  9621  cnfcom3lem  9622  cnfcom3  9623  cnfcom3clem  9624  djuin  9840  infxpenlem  9933  infxpenc  9938  infxpenc2lem2  9940  fseqenlem1  9944  acndom  9971  acndom2  9974  infpwfien  9982  iunfictbso  10034  infmap2  10137  ackbij2lem2  10159  infpssrlem3  10225  infpssrlem4  10226  fin23lem30  10262  isf32lem6  10278  isf32lem7  10279  isf32lem8  10280  enfin1ai  10304  axcc3  10358  axcclem  10377  ttukeylem7  10435  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem8  10559  canthp1lem2  10574  canthp1  10575  pwfseqlem4a  10582  pwfseqlem5  10584  axdc4uzlem  13943  seqf1olem1  14001  seqf1olem2  14002  seqf1o  14003  hashkf  14292  hasheqf1oi  14311  hasheqf1od  14313  hashcl  14316  hashgadd  14337  hashfacen  14414  hashf1lem1  14415  fz1isolem  14421  seqcoll  14424  seqcoll2  14425  cnrecnv  15125  sumeq2ii  15653  summolem3  15674  summolem2a  15675  fsum  15680  fsumf1o  15683  fsumss  15685  fsumcl2lem  15691  fsumadd  15700  fsummulc2  15744  fsumrelem  15768  ackbijnn  15791  prodeq2ii  15874  prodmolem3  15896  prodmolem2a  15897  fprod  15904  fprodf1o  15909  fprodss  15911  fprodser  15912  fprodcl2lem  15913  fprodmul  15923  fproddiv  15924  fprodn0  15942  fproddvdsd  16302  sadcaddlem  16424  sadadd2lem  16426  sadadd3  16428  sadaddlem  16433  sadasslem  16437  sadeq  16439  phimullem  16747  eulerthlem1  16749  eulerthlem2  16750  unbenlem  16877  vdwlem8  16957  0ram  16989  wunndx  17163  xpsaddlem  17535  xpsvsca  17539  xpsle  17541  idfucl  17846  setccatid  18049  setcinv  18055  catcisolem  18075  estrccatid  18096  funcestrcsetclem7  18110  funcestrcsetclem8  18111  funcsetcestrclem7  18125  funcsetcestrclem8  18126  yonffthlem  18246  gsumpropd2lem  18645  mgmhmf1o  18666  idmgmhm  18667  idmhm  18761  mhmf1o  18762  gsumws1  18804  ielefmnd  18853  idghm  19204  ghmf1o  19221  symgbas  19345  elsymgbas  19347  symgbasf  19349  symgbasfi  19352  symg1bas  19364  symggrp  19373  lactghmga  19378  symgfixf1  19410  f1omvdmvd  19416  f1omvdconj  19419  f1omvdco2  19421  pmtrfconj  19439  symggen  19443  pmtrdifellem1  19449  pmtrdifellem2  19450  psgnunilem1  19466  gsumval3eu  19877  gsumval3lem1  19878  gsumval3  19880  gsumzf1o  19885  gsumconst  19907  gsumsub  19921  gsumcom2  19948  dprdfsub  19996  dprdf1o  20007  dprdsn  20011  ablfaclem2  20061  rngisomfv1  20443  rngisom1  20444  rngisomring1  20446  fidomndrnglem  20751  srngcl  20828  lmhmf1o  21043  gsumfsum  21416  zntoslem  21538  islinds2  21795  lindsmm  21810  psrass1lem  21915  psrnegcl  21936  psrlinv  21937  coe1f2  22201  coe1add  22257  evls1rhmlem  22314  evl1sca  22327  pf1ind  22348  mat1dimelbas  22461  mat1f  22472  mdetleib2  22578  mdetrsca  22593  mdetralt  22598  mdetunilem7  22608  mdetunilem9  22610  ssidcn  23245  hmphdis  23786  indishmph  23788  cmphaushmeo  23790  ordthmeolem  23791  txhmeo  23793  qtopf1  23806  ufldom  23952  symgtgp  24096  tsmsf1o  24135  iducn  24272  imasdsf1olem  24363  xpsdsval  24371  imasf1obl  24478  icchmeo  24933  iccpnfcnv  24936  xrhmeo  24938  cnheiborlem  24946  ovolctb  25482  ovoliunlem1  25494  ovoliunlem2  25495  iunmbl2  25549  dyadmbl  25592  vitalilem2  25601  vitalilem3  25602  vitalilem4  25603  vitalilem5  25604  mbfid  25627  dvid  25910  dvexp  25945  dvcnvlem  25968  dvcnv  25969  dvcnvrelem2  26010  dvcnvre  26011  efcvx  26439  reefgim  26440  efif1olem4  26534  eff1olem  26537  logrncl  26556  relogcl  26564  dvrelog  26626  relogcn  26627  logcn  26636  logf1o2  26639  dvlog  26640  dvlog2  26642  advlog  26643  advlogexp  26644  logtayl  26649  logccv  26652  dvcxp1  26729  loglesqrt  26750  asinrebnd  26890  dvatan  26924  efrlim  26958  amgmlem  26978  lgamcvg2  27043  wilthlem2  27057  wilthlem3  27058  sqff1o  27170  lgsqrlem4  27337  logdivsum  27521  log2sumbnd  27532  isismt  28627  motcl  28632  motco  28633  cnvmot  28634  motgrp  28636  motcgrg  28637  f1otrg  28964  f1otrge  28965  axlowdimlem10  29045  axcontlem5  29062  axcontlem10  29067  uspgriedgedg  29270  upgrres1  29407  umgrres1  29408  upgriseupth  30302  pliguhgr  30582  dmadjrn  31991  unopnorm  32013  unopadj  32015  unoplin  32016  counop  32017  idcnop  32077  idhmop  32078  unopbd  32111  bracnln  32205  cnvbraval  32206  leopnmid  32234  nmopleid  32235  hmopidmch  32249  hmopidmpj  32250  disjrdx  32687  fmptco1f1o  32732  isoun  32801  padct  32817  fcobij  32819  fcobijfs  32820  fcobijfs2  32821  wrdpmcl  33024  ccatws1f1o  33037  ccatws1f1olast  33038  mndlactf1o  33116  mndractf1o  33117  abliso  33122  symgfcoeu  33170  symgcom  33171  pmtrcnel  33177  pmtrcnel2  33178  pmtrcnelor  33179  wrdpmtrlast  33181  cycpmco2f1  33212  cycpmco2rn  33213  cycpmco2lem2  33215  cycpmco2lem3  33216  cycpmco2lem4  33217  cycpmco2lem5  33218  cycpmco2lem6  33219  cycpmco2lem7  33220  cycpmco2  33221  cycpmconjv  33230  cycpmconjslem1  33242  cycpmconjslem2  33243  cycpmconjs  33244  islinds5  33457  ellspds  33458  1arithidomlem1  33625  1arithidomlem2  33626  1arithidom  33627  0mplrim  33705  selvply1rhmlemb  33710  mplvrpmlem  33734  mplvrpmfgalem  33735  mplvrpmmhm  33737  mplvrpmrhm  33738  esplyfval0  33755  esplylem  33757  esplympl  33758  esplymhp  33759  esplyfv1  33760  esplyfv  33761  esplysply  33762  esplyfval3  33763  vieta  33771  tpr2rico  34103  xrge0iifmhm  34130  xrge0pluscn  34131  rrhre  34212  esumf1o  34241  volmeas  34422  eulerpartgbij  34563  eulerpartlemmf  34566  eulerpartlemgvv  34567  eulerpartlemgf  34570  eulerpartlemgs2  34571  eulerpartlemn  34572  ballotlemsima  34707  reprpmtf1o  34817  logdivsqrle  34841  hgt750lemg  34845  vonf1owev  35343  deranglem  35401  derangsn  35405  derangenlem  35406  subfacp1lem4  35418  subfacp1lem5  35419  subfacp1lem6  35420  cvmfolem  35514  cvmliftlem6  35525  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem9  38003  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem26  38020  poimirlem27  38021  poimirlem28  38022  poimirlem32  38026  mblfinlem2  38032  dvasin  38078  f1ocan1fv  38100  metf1o  38129  ismtyval  38174  isismty  38175  ismtyima  38177  ismtyhmeolem  38178  ismtybndlem  38180  ismrer1  38212  reheibor  38213  grposnOLD  38256  rngoisocnv  38355  lflnegl  39575  lautset  40581  islaut  40582  lautcl  40586  lautco  40596  pautsetN  40597  ispautN  40598  ldilco  40615  ltrncoidN  40627  ltrncoval  40644  trlcoabs2N  41221  trlcoat  41222  trlcone  41227  cdlemg47a  41233  cdlemg46  41234  cdlemg47  41235  trljco  41239  tgrpgrplem  41248  tendoidcl  41268  tendo0co2  41287  tendo0pl  41290  cdlemi2  41318  cdlemk2  41331  cdlemk4  41333  cdlemk8  41337  cdlemkid2  41423  cdlemk45  41446  cdlemk53b  41455  cdlemk53  41456  cdlemk55a  41458  erng1r  41494  tendocnv  41520  dvalveclem  41524  dva0g  41526  dvhgrp  41606  dvh0g  41610  dvhopN  41615  cdlemn3  41696  cdlemn8  41703  cdlemn9  41704  dihordlem7b  41714  dihopelvalcpre  41747  dihmeetlem1N  41789  dihglblem5apreN  41790  lcfrlem13  42054  hvmapclN  42263  hvmapcl2  42265  dvrelog2  42556  dvrelog3  42557  sticksstones3  42640  sticksstones17  42655  sticksstones18  42656  sticksstones19  42657  readvrec2  42845  readvrec  42846  mapfzcons  43172  mzpresrename  43206  diophrw  43215  eldioph2  43218  diophren  43265  kelac1  43515  imasgim  43552  lnrfg  43571  nvocnvb  43873  brco2f1o  44483  brco3f1o  44484  clsneikex  44557  clsneinex  44558  clsneiel1  44559  neicvgmex  44568  neicvgel1  44570  dssmapntrcls  44579  stoweidlem27  46477  stoweidlem31  46481  stoweidlem39  46489  fourierdlem20  46577  fourierdlem50  46606  fourierdlem52  46608  fourierdlem54  46610  fourierdlem64  46620  fourierdlem76  46632  fourierdlem102  46658  fourierdlem114  46670  sge0f1o  46832  nnfoctbdjlem  46905  isomenndlem  46980  ovnsubaddlem1  47020  3f1oss1  47545  reuf1odnf  47577  reuf1od  47578  f1oresf1o2  47761  fundcmpsurbijinjpreimafv  47889  fundcmpsurinjimaid  47893  grimfn  48377  isgrim  48380  grimuhgr  48385  grimco  48387  uhgrimedgi  48388  isuspgrim0lem  48391  isuspgrim0  48392  isuspgrim  48394  upgrimwlklem4  48398  gricushgr  48415  isubgrgrim  48427  uhgrimisgrgriclem  48428  uhgrimisgrgric  48429  clnbgrgrim  48432  grimedg  48433  grtriclwlk3  48443  isubgr3stgrlem3  48466  isubgr3stgrlem4  48467  isubgr3stgrlem6  48469  isubgr3stgrlem7  48470  isubgr3stgrlem8  48471  isubgr3stgrlem9  48472  grlimfn  48477  isgrlim  48480  uspgrlimlem1  48486  uspgrlimlem2  48487  uspgrlimlem3  48488  uspgrlimlem4  48489  grlimprclnbgredg  48495  grlimgredgex  48498  grlimgrtrilem2  48500  grlictr  48513  clnbgr3stgrgrlim  48517  clnbgr3stgrgrlic  48518  1hegrlfgr  48630  funcringcsetcALTV2lem8  48795  funcringcsetclem8ALTV  48818  itcovalendof  49167  uptrlem1  49707  uptr2  49718  swapf2f1oaALT  49775  swapfcoa  49778  swapffunc  49779  fucoppc  49907  thincciso  49950  thinccisod  49951  lmdran  50168  cmdlan  50169  amgmwlem  50299