Theorem f1of 6862

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

Syntax hints:   → wi 4  ⟶wf 6569  –1-1→wf1 6570  –1-1-onto→wf1o 6572

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 207  df-an 396  df-f1 6578  df-f1o 6580

This theorem is referenced by:  f1ofn  6863  f1ompt  7145  f1oresrab  7161  fsn  7169  fsnunf  7219  f1ocnvfv1  7312  f1ocnvfv2  7313  fsnex  7319  f1ocnvdm  7321  fcof1oinvd  7329  fveqf1o  7338  isocnv  7366  isocnv3  7368  isores2  7369  isotr  7372  isofr2  7380  isopolem  7381  isosolem  7383  f1oiso2  7388  weniso  7390  f1ofveu  7442  f1oexrnex  7967  f1oabexg  7980  f1oabexgOLD  7981  wemoiso  8014  mptcnfimad  8027  suppsnop  8219  smoiso  8418  mapsnd  8944  ralxpmap  8954  f1oen2g  9028  en1  9086  en1OLD  9087  enfixsn  9147  mapen  9207  ac6sfi  9348  domunfican  9389  fiint  9394  fiintOLD  9395  mapfienlem1  9474  mapfienlem2  9475  mapfienlem3  9476  mapfien  9477  supisoex  9543  supiso  9544  ordiso2  9584  unxpwdom2  9657  cantnfle  9740  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1d  9757  cantnflem1  9758  cnfcomlem  9768  cnfcom  9769  cnfcom2lem  9770  cnfcom2  9771  cnfcom3lem  9772  cnfcom3  9773  cnfcom3clem  9774  djuin  9987  infxpenlem  10082  infxpenc  10087  infxpenc2lem2  10089  fseqenlem1  10093  acndom  10120  acndom2  10123  infpwfien  10131  iunfictbso  10183  infmap2  10286  ackbij2lem2  10308  infpssrlem3  10374  infpssrlem4  10375  fin23lem30  10411  isf32lem6  10427  isf32lem7  10428  isf32lem8  10429  enfin1ai  10453  axcc3  10507  axcclem  10526  ttukeylem7  10584  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  canthp1lem2  10722  canthp1  10723  pwfseqlem4a  10730  pwfseqlem5  10732  axdc4uzlem  14034  seqf1olem1  14092  seqf1olem2  14093  seqf1o  14094  hashkf  14381  hasheqf1oi  14400  hasheqf1od  14402  hashcl  14405  hashgadd  14426  hashfacen  14503  hashf1lem1  14504  fz1isolem  14510  seqcoll  14513  seqcoll2  14514  cnrecnv  15214  sumeq2ii  15741  summolem3  15762  summolem2a  15763  fsum  15768  fsumf1o  15771  fsumss  15773  fsumcl2lem  15779  fsumadd  15788  fsummulc2  15832  fsumrelem  15855  ackbijnn  15876  prodeq2ii  15959  prodmolem3  15981  prodmolem2a  15982  fprod  15989  fprodf1o  15994  fprodss  15996  fprodser  15997  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodn0  16027  fproddvdsd  16383  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  phimullem  16826  eulerthlem1  16828  eulerthlem2  16829  unbenlem  16955  vdwlem8  17035  0ram  17067  wunndx  17242  xpsaddlem  17633  xpsvsca  17637  xpsle  17639  idfucl  17945  setccatid  18151  setcinv  18157  catcisolem  18177  estrccatid  18200  funcestrcsetclem7  18215  funcestrcsetclem8  18216  funcsetcestrclem7  18230  funcsetcestrclem8  18231  yonffthlem  18352  gsumpropd2lem  18717  mgmhmf1o  18738  idmgmhm  18739  idmhm  18830  mhmf1o  18831  gsumws1  18873  ielefmnd  18922  idghm  19271  ghmf1o  19288  symgbas  19413  elsymgbas  19415  symgbasf  19417  symgbasfi  19420  symg1bas  19432  symggrp  19442  lactghmga  19447  symgfixf1  19479  f1omvdmvd  19485  f1omvdconj  19488  f1omvdco2  19490  pmtrfconj  19508  symggen  19512  pmtrdifellem1  19518  pmtrdifellem2  19519  psgnunilem1  19535  gsumval3eu  19946  gsumval3lem1  19947  gsumval3  19949  gsumzf1o  19954  gsumconst  19976  gsumsub  19990  gsumcom2  20017  dprdfsub  20065  dprdf1o  20076  dprdsn  20080  ablfaclem2  20130  rngisomfv1  20491  rngisom1  20492  rngisomring1  20494  fidomndrnglem  20795  srngcl  20872  lmhmf1o  21068  gsumfsum  21475  zntoslem  21598  islinds2  21856  lindsmm  21871  psrass1lem  21975  psrnegcl  21997  psrlinv  21998  coe1f2  22232  coe1add  22288  evls1rhmlem  22346  evl1sca  22359  pf1ind  22380  mat1dimelbas  22498  mat1f  22509  mdetleib2  22615  mdetrsca  22630  mdetralt  22635  mdetunilem7  22645  mdetunilem9  22647  ssidcn  23284  hmphdis  23825  indishmph  23827  cmphaushmeo  23829  ordthmeolem  23830  txhmeo  23832  qtopf1  23845  ufldom  23991  symgtgp  24135  tsmsf1o  24174  iducn  24313  imasdsf1olem  24404  xpsdsval  24412  imasf1obl  24522  icchmeo  24990  icchmeoOLD  24991  iccpnfcnv  24994  xrhmeo  24996  cnheiborlem  25005  ovolctb  25544  ovoliunlem1  25556  ovoliunlem2  25557  iunmbl2  25611  dyadmbl  25654  vitalilem2  25663  vitalilem3  25664  vitalilem4  25665  vitalilem5  25666  mbfid  25689  dvid  25973  dvexp  26011  dvcnvlem  26034  dvcnv  26035  dvcnvrelem2  26077  dvcnvre  26078  efcvx  26511  reefgim  26512  efif1olem4  26605  eff1olem  26608  logrncl  26627  relogcl  26635  dvrelog  26697  relogcn  26698  logcn  26707  logf1o2  26710  dvlog  26711  dvlog2  26713  advlog  26714  advlogexp  26715  logtayl  26720  logccv  26723  dvcxp1  26800  loglesqrt  26822  asinrebnd  26962  dvatan  26996  efrlim  27030  efrlimOLD  27031  amgmlem  27051  lgamcvg2  27116  wilthlem2  27130  wilthlem3  27131  sqff1o  27243  lgsqrlem4  27411  logdivsum  27595  log2sumbnd  27606  isismt  28560  motcl  28565  motco  28566  cnvmot  28567  motgrp  28569  motcgrg  28570  f1otrg  28897  f1otrge  28898  axlowdimlem10  28984  axcontlem5  29001  axcontlem10  29006  uspgriedgedg  29211  upgrres1  29348  umgrres1  29349  upgriseupth  30239  pliguhgr  30518  dmadjrn  31927  unopnorm  31949  unopadj  31951  unoplin  31952  counop  31953  idcnop  32013  idhmop  32014  unopbd  32047  bracnln  32141  cnvbraval  32142  leopnmid  32170  nmopleid  32171  hmopidmch  32185  hmopidmpj  32186  disjrdx  32613  fmptco1f1o  32652  isoun  32713  padct  32733  fcobij  32736  fcobijfs  32737  wrdpmcl  32904  ccatws1f1o  32918  ccatws1f1olast  32919  mndlactf1o  33016  mndractf1o  33017  abliso  33022  symgfcoeu  33075  symgcom  33076  pmtrcnel  33082  pmtrcnel2  33083  pmtrcnelor  33084  wrdpmtrlast  33086  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  cycpmconjv  33135  cycpmconjslem1  33147  cycpmconjslem2  33148  cycpmconjs  33149  islinds5  33360  ellspds  33361  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  tpr2rico  33858  xrge0iifmhm  33885  xrge0pluscn  33886  rrhre  33967  esumf1o  34014  volmeas  34195  eulerpartgbij  34337  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgf  34344  eulerpartlemgs2  34345  eulerpartlemn  34346  ballotlemsima  34480  reprpmtf1o  34603  logdivsqrle  34627  hgt750lemg  34631  deranglem  35134  derangsn  35138  derangenlem  35139  subfacp1lem4  35151  subfacp1lem5  35152  subfacp1lem6  35153  cvmfolem  35247  cvmliftlem6  35258  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem32  37612  mblfinlem2  37618  dvasin  37664  f1ocan1fv  37686  metf1o  37715  ismtyval  37760  isismty  37761  ismtyima  37763  ismtyhmeolem  37764  ismtybndlem  37766  ismrer1  37798  reheibor  37799  grposnOLD  37842  rngoisocnv  37941  lflnegl  39032  lautset  40039  islaut  40040  lautcl  40044  lautco  40054  pautsetN  40055  ispautN  40056  ldilco  40073  ltrncoidN  40085  ltrncoval  40102  trlcoabs2N  40679  trlcoat  40680  trlcone  40685  cdlemg47a  40691  cdlemg46  40692  cdlemg47  40693  trljco  40697  tgrpgrplem  40706  tendoidcl  40726  tendo0co2  40745  tendo0pl  40748  cdlemi2  40776  cdlemk2  40789  cdlemk4  40791  cdlemk8  40795  cdlemkid2  40881  cdlemk45  40904  cdlemk53b  40913  cdlemk53  40914  cdlemk55a  40916  erng1r  40952  tendocnv  40978  dvalveclem  40982  dva0g  40984  dvhgrp  41064  dvh0g  41068  dvhopN  41073  cdlemn3  41154  cdlemn8  41161  cdlemn9  41162  dihordlem7b  41172  dihopelvalcpre  41205  dihmeetlem1N  41247  dihglblem5apreN  41248  lcfrlem13  41512  hvmapclN  41721  hvmapcl2  41723  dvrelog2  42021  dvrelog3  42022  sticksstones3  42105  sticksstones17  42120  sticksstones18  42121  sticksstones19  42122  metakunt33  42194  mapfzcons  42672  mzpresrename  42706  diophrw  42715  eldioph2  42718  diophren  42769  kelac1  43020  imasgim  43057  lnrfg  43076  nvocnvb  43384  brco2f1o  43994  brco3f1o  43995  clsneikex  44068  clsneinex  44069  clsneiel1  44070  neicvgmex  44079  neicvgel1  44081  dssmapntrcls  44090  stoweidlem27  45948  stoweidlem31  45952  stoweidlem39  45960  fourierdlem20  46048  fourierdlem50  46077  fourierdlem52  46079  fourierdlem54  46081  fourierdlem64  46091  fourierdlem76  46103  fourierdlem102  46129  fourierdlem114  46141  sge0f1o  46303  nnfoctbdjlem  46376  isomenndlem  46451  ovnsubaddlem1  46491  3f1oss1  46990  reuf1odnf  47022  reuf1od  47023  f1oresf1o2  47206  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjimaid  47285  grimfn  47749  isgrim  47752  isuspgrim0lem  47755  isuspgrim0  47756  uspgrimprop  47757  isuspgrim  47759  grimuhgr  47762  grimco  47764  gricushgr  47770  isubgrgrim  47781  uhgrimisgrgriclem  47782  uhgrimisgrgric  47783  clnbgrgrim  47786  grimedg  47787  grtriclwlk3  47796  grlimfn  47803  isgrlim  47806  uspgrlimlem1  47812  uspgrlimlem2  47813  uspgrlimlem3  47814  uspgrlimlem4  47815  grlimgrtrilem2  47819  grlictr  47832  1hegrlfgr  47855  funcringcsetcALTV2lem8  48020  funcringcsetclem8ALTV  48043  itcovalendof  48403  thincciso  48716  amgmwlem  48896