Theorem f1of 6846

Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of	⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 6845	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶1-1𝐵)
2		f1f 6800	. 2 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 18	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶𝐵)

This proof depends on syntax axioms:   → wi 4  ⟶wf 6554  ⟶1-1wf1 6555  ⟶1-1ontowf1o 6557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f1 6563  df-f1o 6565

This theorem is used by:  f1ofn  6847  f1ompt  7135  f1oresrab  7152  fsn  7160  fsnunf  7213  f1ounsn  7303  f1ocnvfv1  7307  f1ocnvfv2  7308  fsnex  7314  f1ocnvdm  7316  fcof1oinvd  7324  fveqf1o  7333  isocnv  7361  isocnv3  7363  isores2  7364  isotr  7367  isofr2  7375  isopolem  7376  isosolem  7378  f1oiso2  7383  weniso  7387  f1ofveu  7437  f1oexrnex  7963  f1oabexg  7977  wemoiso  8009  mptcnfimad  8022  suppsnop  8223  smoiso  8398  mapsnd  8942  ralxpmap  8952  f1oen2g  9023  en1  9079  enfixsn  9133  mapen  9188  ac6sfi  9303  domunfican  9341  fiint  9346  mapfienlem1  9424  mapfienlem2  9425  mapfienlem3  9426  mapfien  9427  supisoex  9494  supiso  9495  ordiso2  9536  unxpwdom2  9609  cantnfle  9699  cantnfp1lem3  9708  cantnflem1b  9714  cantnflem1d  9716  cantnflem1  9717  cnfcomlem  9727  cnfcom  9728  cnfcom2lem  9729  cnfcom2  9730  cnfcom3lem  9731  cnfcom3  9732  cnfcom3clem  9733  djuin  10026  infxpenlem  10119  infxpenc  10124  infxpenc2lem2  10126  fseqenlem1  10130  acndom  10157  acndom2  10160  infpwfien  10168  iunfictbso  10220  infmap2  10322  ackbij2lem2  10344  infpssrlem3  10410  infpssrlem4  10411  fin23lem30  10447  isf32lem6  10463  isf32lem7  10464  isf32lem8  10465  enfin1ai  10489  axcc3  10543  axcclem  10562  ttukeylem7  10620  fpwwe2lem5  10747  fpwwe2lem6  10748  fpwwe2lem8  10750  canthp1lem2  10765  canthp1  10766  pwfseqlem4a  10773  pwfseqlem5  10775  axdc4uzlem  14153  seqf1olem1  14211  seqf1olem2  14212  seqf1o  14213  hashkf  14503  hasheqf1oi  14522  hasheqf1od  14524  hashcl  14527  hashgadd  14548  hashfacen  14626  hashf1lem1  14627  fz1isolem  14633  seqcoll  14636  seqcoll2  14637  cnrecnv  15361  sumeq2ii  15889  summolem3  15909  summolem2a  15910  fsum  15915  fsumf1o  15918  fsumss  15920  fsumcl2lem  15926  fsumadd  15935  fsummulc2  15979  fsumrelem  16003  ackbijnn  16026  prodeq2ii  16109  prodmolem3  16129  prodmolem2a  16130  fprod  16137  fprodf1o  16142  fprodss  16144  fprodser  16145  fprodcl2lem  16146  fprodmul  16156  fproddiv  16157  fprodn0  16175  fproddvdsd  16534  sadcaddlem  16656  sadadd2lem  16658  sadadd3  16660  sadaddlem  16665  sadasslem  16669  sadeq  16671  phimullem  16985  eulerthlem1  16987  eulerthlem2  16988  unbenlem  17115  vdwlem8  17195  0ram  17227  wunndx  17402  xpsaddlem  17774  xpsvsca  17778  xpsle  17780  idfucl  18085  setccatid  18288  setcinv  18294  catcisolem  18314  estrccatid  18335  funcestrcsetclem7  18349  funcestrcsetclem8  18350  funcsetcestrclem7  18364  funcsetcestrclem8  18365  yonffthlem  18485  gsumpropd2lem  18897  mgmhmf1o  18918  idmgmhm  18919  idmhm  19019  mhmf1o  19020  gsumws1  19063  ielefmnd  19112  idghm  19474  ghmf1o  19491  imasgim  19513  symgbas  19616  elsymgbas  19618  symgbasf  19620  symgbasfi  19623  symg1bas  19635  symggrp  19644  lactghmga  19649  symgfixf1  19681  f1omvdmvd  19687  f1omvdconj  19690  f1omvdco2  19692  pmtrfconj  19710  symggen  19714  pmtrdifellem1  19720  pmtrdifellem2  19721  psgnunilem1  19737  gsumval3eu  20148  gsumval3lem1  20149  gsumval3  20151  gsumzf1o  20156  gsumconst  20178  gsumsub  20192  gsumcom2  20219  dprdfsub  20267  dprdf1o  20278  dprdsn  20282  ablfaclem2  20332  rngisomfv1  20725  rngisom1  20726  rngisomring1  20728  fidomndrnglem  21060  srngcl  21136  lmhmf1o  21351  gsumfsum  21770  zntoslem  21892  islinds2  22149  lindsmm  22164  psrass1lem  22271  psrnegcl  22292  psrlinv  22293  coe1f2  22557  coe1add  22613  evls1rhmlem  22669  evl1sca  22682  pf1ind  22703  mat1dimelbas  22816  mat1f  22827  mdetleib2  22933  mdetrsca  22948  mdetralt  22953  mdetunilem7  22963  mdetunilem9  22965  ssidcn  23603  hmphdis  24145  indishmph  24147  cmphaushmeo  24149  ordthmeolem  24150  txhmeo  24152  qtopf1  24165  ufldom  24311  symgtgp  24455  tsmsf1o  24494  iducn  24631  imasdsf1olem  24722  xpsdsval  24730  imasf1obl  24837  icchmeo  25292  iccpnfcnv  25295  xrhmeo  25297  cnheiborlem  25305  ovolctb  25841  ovoliunlem1  25853  ovoliunlem2  25854  iunmbl2  25908  dyadmbl  25951  vitalilem2  25960  vitalilem3  25961  vitalilem4  25962  vitalilem5  25963  mbfid  25986  dvid  26268  dvexp  26303  dvcnvlem  26326  dvcnv  26327  dvcnvrelem2  26368  dvcnvre  26369  efcvx  26806  reefgim  26807  efif1olem4  26903  eff1olem  26906  logrncl  26925  relogcl  26933  dvrelog  26995  relogcn  26996  logcn  27005  logf1o2  27008  dvlog  27009  dvlog2  27011  advlog  27012  advlogexp  27013  logtayl  27018  logccv  27021  dvcxp1  27098  loglesqrt  27119  asinrebnd  27259  dvatan  27293  efrlim  27327  amgmlem  27347  lgamcvg2  27412  wilthlem2  27426  wilthlem3  27427  sqff1o  27539  lgsqrlem4  27706  logdivsum  27890  log2sumbnd  27901  isismt  29027  motcl  29032  motco  29033  cnvmot  29034  motgrp  29036  motcgrg  29037  f1otrg  29478  f1otrge  29479  axlowdimlem10  29559  axcontlem5  29576  axcontlem10  29581  uspgriedgedg  29787  upgrres1  29924  umgrres1  29925  upgriseupth  30838  pliguhgr  31118  dmadjrn  32527  unopnorm  32549  unopadj  32551  unoplin  32552  counop  32553  idcnop  32613  idhmop  32614  unopbd  32647  bracnln  32741  cnvbraval  32742  leopnmid  32770  nmopleid  32771  hmopidmch  32785  hmopidmpj  32786  disjrdx  33257  fmptco1f1o  33299  isoun  33366  padct  33381  fcobij  33382  fcobijfs  33383  fcobijfs2  33384  wrdpmcl  33575  ccatws1f1o  33584  ccatws1f1olast  33585  mndlactf1o  33661  mndractf1o  33662  abliso  33666  symgfcoeu  33713  symgcom  33714  pmtrcnel  33720  pmtrcnel2  33721  pmtrcnelor  33722  wrdpmtrlast  33724  cycpmco2f1  33755  cycpmco2rn  33756  cycpmco2lem2  33758  cycpmco2lem3  33759  cycpmco2lem4  33760  cycpmco2lem5  33761  cycpmco2lem6  33762  cycpmco2lem7  33763  cycpmco2  33764  cycpmconjv  33773  cycpmconjslem1  33785  cycpmconjslem2  33786  cycpmconjs  33787  islinds5  33993  ellspds  33994  1arithidomlem1  34137  1arithidomlem2  34138  1arithidom  34139  0mplrim  34216  selvply1rhmlemb  34221  mplvrpmlem  34245  mplvrpmfgalem  34246  mplvrpmmhm  34248  mplvrpmrhm  34249  esplyfval0  34266  esplylem  34268  esplympl  34269  esplymhp  34270  esplyfv1  34271  esplyfv  34272  esplysply  34273  esplyfval3  34274  vieta  34282  tpr2rico  34614  xrge0iifmhm  34641  xrge0pluscn  34642  rrhre  34723  esumf1o  34752  volmeas  34934  eulerpartgbij  35074  eulerpartlemmf  35077  eulerpartlemgvv  35078  eulerpartlemgf  35081  eulerpartlemgs2  35082  eulerpartlemn  35083  ballotlemsima  35218  reprpmtf1o  35325  logdivsqrle  35349  hgt750lemg  35353  j00smo  36005  maxssj0  36006  j0ltalephlem  36007  j0ltaleph  36008  jf1  36010  dfk12  36012  dfk22  36013  dfk32  36014  j0le  36019  k3n0j0lt  36020  jltalephlem  36025  jltaleph  36026  vonf1owevOLD  36038  deranglem  36098  derangsn  36102  derangenlem  36103  subfacp1lem4  36115  subfacp1lem5  36116  subfacp1lem6  36117  cvmfolem  36211  cvmliftlem6  36222  poimirlem1  38731  poimirlem2  38732  poimirlem3  38733  poimirlem4  38734  poimirlem6  38736  poimirlem7  38737  poimirlem9  38739  poimirlem11  38741  poimirlem12  38742  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem22  38752  poimirlem26  38756  poimirlem27  38757  poimirlem28  38758  poimirlem32  38762  mblfinlem2  38768  dvasin  38814  f1ocan1fv  38852  metf1o  38881  ismtyval  38926  isismty  38927  ismtyima  38929  ismtyhmeolem  38930  ismtybndlem  38932  ismrer1  38964  reheibor  38965  grposnOLD  39008  rngoisocnv  39107  lflnegl  40325  lautset  41331  islaut  41332  lautcl  41336  lautco  41346  pautsetN  41347  ispautN  41348  ldilco  41365  ltrncoidN  41377  ltrncoval  41394  trlcoabs2N  41971  trlcoat  41972  trlcone  41977  cdlemg47a  41983  cdlemg46  41984  cdlemg47  41985  trljco  41989  tgrpgrplem  41998  tendoidcl  42018  tendo0co2  42037  tendo0pl  42040  cdlemi2  42068  cdlemk2  42081  cdlemk4  42083  cdlemk8  42087  cdlemkid2  42173  cdlemk45  42196  cdlemk53b  42205  cdlemk53  42206  cdlemk55a  42208  erng1r  42244  tendocnv  42270  dvalveclem  42274  dva0g  42276  dvhgrp  42356  dvh0g  42360  dvhopN  42365  cdlemn3  42446  cdlemn8  42453  cdlemn9  42454  dihordlem7b  42464  dihopelvalcpre  42497  dihmeetlem1N  42539  dihglblem5apreN  42540  lcfrlem13  42804  hvmapclN  43013  hvmapcl2  43015  dvrelog2  43306  dvrelog3  43307  sticksstones3  43390  sticksstones17  43405  sticksstones18  43406  sticksstones19  43407  readvrec2  43605  readvrec  43606  mapfzcons  43920  mzpresrename  43954  diophrw  43963  eldioph2  43966  diophren  44013  kelac1  44258  lnrfg  44313  nvocnvb  44615  brco2f1o  45224  brco3f1o  45225  clsneikex  45298  clsneinex  45299  clsneiel1  45300  neicvgmex  45309  neicvgel1  45311  dssmapntrcls  45320  hfstructwe  46234  stoweidlem27  47242  stoweidlem31  47246  stoweidlem39  47254  fourierdlem20  47342  fourierdlem50  47371  fourierdlem52  47373  fourierdlem54  47375  fourierdlem64  47385  fourierdlem76  47397  fourierdlem102  47423  fourierdlem114  47435  sge0f1o  47597  nnfoctbdjlem  47670  isomenndlem  47745  ovnsubaddlem1  47785  3f1oss1  48350  reuf1odnf  48383  reuf1od  48384  f1oresf1o2  48566  fundcmpsurbijinjpreimafv  48694  fundcmpsurinjimaid  48698  grimfn  49182  isgrim  49185  grimuhgr  49190  grimco  49192  uhgrimedgi  49193  isuspgrim0lem  49196  isuspgrim0  49197  isuspgrim  49199  upgrimwlklem4  49203  gricushgr  49220  isubgrgrim  49232  uhgrimisgrgriclem  49233  uhgrimisgrgric  49234  clnbgrgrim  49237  grimedg  49238  grtriclwlk3  49248  isubgr3stgrlem3  49271  isubgr3stgrlem4  49272  isubgr3stgrlem6  49274  isubgr3stgrlem7  49275  isubgr3stgrlem8  49276  isubgr3stgrlem9  49277  grlimfn  49282  isgrlim  49285  uspgrlimlem1  49291  uspgrlimlem2  49292  uspgrlimlem3  49293  uspgrlimlem4  49294  grlimprclnbgredg  49300  grlimgredgex  49303  grlimgrtrilem2  49305  grlictr  49318  clnbgr3stgrgrlim  49322  clnbgr3stgrgrlic  49323  1hegrlfgr  49435  funcringcsetcALTV2lem8  49599  funcringcsetclem8ALTV  49622  itcovalendof  49986  uptrlem1  50531  uptr2  50542  swapf2f1oaALT  50605  swapfcoa  50608  swapffunc  50609  fucoppc  50750  thincciso  50793  thinccisod  50794  parmapfunc2  50979  parmapfunc  50980  lmdran  51059  cmdlan  51060  amgmwlem  51267