Theorem f1of 6782

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

Syntax hints:   → wi 4  ⟶wf 6496  –1-1→wf1 6497  –1-1-onto→wf1o 6499

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 6505  df-f1o 6507

This theorem is referenced by:  f1ofn  6783  f1ompt  7065  f1oresrab  7082  fsn  7090  fsnunf  7141  f1ounsn  7228  f1ocnvfv1  7232  f1ocnvfv2  7233  fsnex  7239  f1ocnvdm  7241  fcof1oinvd  7249  fveqf1o  7258  isocnv  7286  isocnv3  7288  isores2  7289  isotr  7292  isofr2  7300  isopolem  7301  isosolem  7303  f1oiso2  7308  weniso  7310  f1ofveu  7362  f1oexrnex  7879  f1oabexg  7894  f1oabexgOLD  7895  wemoiso  7927  mptcnfimad  7940  suppsnop  8130  smoiso  8304  mapsnd  8836  ralxpmap  8846  f1oen2g  8917  en1  8973  enfixsn  9026  mapen  9081  ac6sfi  9196  domunfican  9234  fiint  9239  mapfienlem1  9320  mapfienlem2  9321  mapfienlem3  9322  mapfien  9323  supisoex  9390  supiso  9391  ordiso2  9432  unxpwdom2  9505  cantnfle  9592  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  cnfcom3clem  9626  djuin  9842  infxpenlem  9935  infxpenc  9940  infxpenc2lem2  9942  fseqenlem1  9946  acndom  9973  acndom2  9976  infpwfien  9984  iunfictbso  10036  infmap2  10139  ackbij2lem2  10161  infpssrlem3  10227  infpssrlem4  10228  fin23lem30  10264  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  enfin1ai  10306  axcc3  10360  axcclem  10379  ttukeylem7  10437  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  canthp1lem2  10576  canthp1  10577  pwfseqlem4a  10584  pwfseqlem5  10586  axdc4uzlem  13918  seqf1olem1  13976  seqf1olem2  13977  seqf1o  13978  hashkf  14267  hasheqf1oi  14286  hasheqf1od  14288  hashcl  14291  hashgadd  14312  hashfacen  14389  hashf1lem1  14390  fz1isolem  14396  seqcoll  14399  seqcoll2  14400  cnrecnv  15100  sumeq2ii  15628  summolem3  15649  summolem2a  15650  fsum  15655  fsumf1o  15658  fsumss  15660  fsumcl2lem  15666  fsumadd  15675  fsummulc2  15719  fsumrelem  15742  ackbijnn  15763  prodeq2ii  15846  prodmolem3  15868  prodmolem2a  15869  fprod  15876  fprodf1o  15881  fprodss  15883  fprodser  15884  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodn0  15914  fproddvdsd  16274  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  sadeq  16411  phimullem  16718  eulerthlem1  16720  eulerthlem2  16721  unbenlem  16848  vdwlem8  16928  0ram  16960  wunndx  17134  xpsaddlem  17506  xpsvsca  17510  xpsle  17512  idfucl  17817  setccatid  18020  setcinv  18026  catcisolem  18046  estrccatid  18067  funcestrcsetclem7  18081  funcestrcsetclem8  18082  funcsetcestrclem7  18096  funcsetcestrclem8  18097  yonffthlem  18217  gsumpropd2lem  18616  mgmhmf1o  18637  idmgmhm  18638  idmhm  18732  mhmf1o  18733  gsumws1  18775  ielefmnd  18824  idghm  19172  ghmf1o  19189  symgbas  19313  elsymgbas  19315  symgbasf  19317  symgbasfi  19320  symg1bas  19332  symggrp  19341  lactghmga  19346  symgfixf1  19378  f1omvdmvd  19384  f1omvdconj  19387  f1omvdco2  19389  pmtrfconj  19407  symggen  19411  pmtrdifellem1  19417  pmtrdifellem2  19418  psgnunilem1  19434  gsumval3eu  19845  gsumval3lem1  19846  gsumval3  19848  gsumzf1o  19853  gsumconst  19875  gsumsub  19889  gsumcom2  19916  dprdfsub  19964  dprdf1o  19975  dprdsn  19979  ablfaclem2  20029  rngisomfv1  20413  rngisom1  20414  rngisomring1  20416  fidomndrnglem  20717  srngcl  20794  lmhmf1o  21010  gsumfsum  21401  zntoslem  21523  islinds2  21780  lindsmm  21795  psrass1lem  21900  psrnegcl  21922  psrlinv  21923  coe1f2  22162  coe1add  22218  evls1rhmlem  22277  evl1sca  22290  pf1ind  22311  mat1dimelbas  22427  mat1f  22438  mdetleib2  22544  mdetrsca  22559  mdetralt  22564  mdetunilem7  22574  mdetunilem9  22576  ssidcn  23211  hmphdis  23752  indishmph  23754  cmphaushmeo  23756  ordthmeolem  23757  txhmeo  23759  qtopf1  23772  ufldom  23918  symgtgp  24062  tsmsf1o  24101  iducn  24238  imasdsf1olem  24329  xpsdsval  24337  imasf1obl  24444  icchmeo  24906  icchmeoOLD  24907  iccpnfcnv  24910  xrhmeo  24912  cnheiborlem  24921  ovolctb  25459  ovoliunlem1  25471  ovoliunlem2  25472  iunmbl2  25526  dyadmbl  25569  vitalilem2  25578  vitalilem3  25579  vitalilem4  25580  vitalilem5  25581  mbfid  25604  dvid  25887  dvexp  25925  dvcnvlem  25948  dvcnv  25949  dvcnvrelem2  25991  dvcnvre  25992  efcvx  26427  reefgim  26428  efif1olem4  26522  eff1olem  26525  logrncl  26544  relogcl  26552  dvrelog  26614  relogcn  26615  logcn  26624  logf1o2  26627  dvlog  26628  dvlog2  26630  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  loglesqrt  26739  asinrebnd  26879  dvatan  26913  efrlim  26947  efrlimOLD  26948  amgmlem  26968  lgamcvg2  27033  wilthlem2  27047  wilthlem3  27048  sqff1o  27160  lgsqrlem4  27328  logdivsum  27512  log2sumbnd  27523  isismt  28618  motcl  28623  motco  28624  cnvmot  28625  motgrp  28627  motcgrg  28628  f1otrg  28955  f1otrge  28956  axlowdimlem10  29036  axcontlem5  29053  axcontlem10  29058  uspgriedgedg  29261  upgrres1  29398  umgrres1  29399  upgriseupth  30294  pliguhgr  30573  dmadjrn  31982  unopnorm  32004  unopadj  32006  unoplin  32007  counop  32008  idcnop  32068  idhmop  32069  unopbd  32102  bracnln  32196  cnvbraval  32197  leopnmid  32225  nmopleid  32226  hmopidmch  32240  hmopidmpj  32241  disjrdx  32677  fmptco1f1o  32722  isoun  32791  padct  32807  fcobij  32809  fcobijfs  32810  fcobijfs2  32811  wrdpmcl  33030  ccatws1f1o  33043  ccatws1f1olast  33044  mndlactf1o  33122  mndractf1o  33123  abliso  33128  symgfcoeu  33175  symgcom  33176  pmtrcnel  33182  pmtrcnel2  33183  pmtrcnelor  33184  wrdpmtrlast  33186  cycpmco2f1  33217  cycpmco2rn  33218  cycpmco2lem2  33220  cycpmco2lem3  33221  cycpmco2lem4  33222  cycpmco2lem5  33223  cycpmco2lem6  33224  cycpmco2lem7  33225  cycpmco2  33226  cycpmconjv  33235  cycpmconjslem1  33247  cycpmconjslem2  33248  cycpmconjs  33249  islinds5  33459  ellspds  33460  1arithidomlem1  33627  1arithidomlem2  33628  1arithidom  33629  mplvrpmlem  33719  mplvrpmfgalem  33720  mplvrpmmhm  33722  mplvrpmrhm  33723  esplyfval0  33740  esplylem  33742  esplympl  33743  esplymhp  33744  esplyfv1  33745  esplyfv  33746  esplysply  33747  esplyfval3  33748  vieta  33756  tpr2rico  34089  xrge0iifmhm  34116  xrge0pluscn  34117  rrhre  34198  esumf1o  34227  volmeas  34408  eulerpartgbij  34549  eulerpartlemmf  34552  eulerpartlemgvv  34553  eulerpartlemgf  34556  eulerpartlemgs2  34557  eulerpartlemn  34558  ballotlemsima  34693  reprpmtf1o  34803  logdivsqrle  34827  hgt750lemg  34831  vonf1owev  35321  deranglem  35379  derangsn  35383  derangenlem  35384  subfacp1lem4  35396  subfacp1lem5  35397  subfacp1lem6  35398  cvmfolem  35492  cvmliftlem6  35503  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem4  37869  poimirlem6  37871  poimirlem7  37872  poimirlem9  37874  poimirlem11  37876  poimirlem12  37877  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem26  37891  poimirlem27  37892  poimirlem28  37893  poimirlem32  37897  mblfinlem2  37903  dvasin  37949  f1ocan1fv  37971  metf1o  38000  ismtyval  38045  isismty  38046  ismtyima  38048  ismtyhmeolem  38049  ismtybndlem  38051  ismrer1  38083  reheibor  38084  grposnOLD  38127  rngoisocnv  38226  lflnegl  39446  lautset  40452  islaut  40453  lautcl  40457  lautco  40467  pautsetN  40468  ispautN  40469  ldilco  40486  ltrncoidN  40498  ltrncoval  40515  trlcoabs2N  41092  trlcoat  41093  trlcone  41098  cdlemg47a  41104  cdlemg46  41105  cdlemg47  41106  trljco  41110  tgrpgrplem  41119  tendoidcl  41139  tendo0co2  41158  tendo0pl  41161  cdlemi2  41189  cdlemk2  41202  cdlemk4  41204  cdlemk8  41208  cdlemkid2  41294  cdlemk45  41317  cdlemk53b  41326  cdlemk53  41327  cdlemk55a  41329  erng1r  41365  tendocnv  41391  dvalveclem  41395  dva0g  41397  dvhgrp  41477  dvh0g  41481  dvhopN  41486  cdlemn3  41567  cdlemn8  41574  cdlemn9  41575  dihordlem7b  41585  dihopelvalcpre  41618  dihmeetlem1N  41660  dihglblem5apreN  41661  lcfrlem13  41925  hvmapclN  42134  hvmapcl2  42136  dvrelog2  42428  dvrelog3  42429  sticksstones3  42512  sticksstones17  42527  sticksstones18  42528  sticksstones19  42529  readvrec2  42725  readvrec  42726  mapfzcons  43067  mzpresrename  43101  diophrw  43110  eldioph2  43113  diophren  43164  kelac1  43414  imasgim  43451  lnrfg  43470  nvocnvb  43772  brco2f1o  44382  brco3f1o  44383  clsneikex  44456  clsneinex  44457  clsneiel1  44458  neicvgmex  44467  neicvgel1  44469  dssmapntrcls  44478  stoweidlem27  46379  stoweidlem31  46383  stoweidlem39  46391  fourierdlem20  46479  fourierdlem50  46508  fourierdlem52  46510  fourierdlem54  46512  fourierdlem64  46522  fourierdlem76  46534  fourierdlem102  46560  fourierdlem114  46572  sge0f1o  46734  nnfoctbdjlem  46807  isomenndlem  46882  ovnsubaddlem1  46922  3f1oss1  47429  reuf1odnf  47461  reuf1od  47462  f1oresf1o2  47645  fundcmpsurbijinjpreimafv  47761  fundcmpsurinjimaid  47765  grimfn  48233  isgrim  48236  grimuhgr  48241  grimco  48243  uhgrimedgi  48244  isuspgrim0lem  48247  isuspgrim0  48248  isuspgrim  48250  upgrimwlklem4  48254  gricushgr  48271  isubgrgrim  48283  uhgrimisgrgriclem  48284  uhgrimisgrgric  48285  clnbgrgrim  48288  grimedg  48289  grtriclwlk3  48299  isubgr3stgrlem3  48322  isubgr3stgrlem4  48323  isubgr3stgrlem6  48325  isubgr3stgrlem7  48326  isubgr3stgrlem8  48327  isubgr3stgrlem9  48328  grlimfn  48333  isgrlim  48336  uspgrlimlem1  48342  uspgrlimlem2  48343  uspgrlimlem3  48344  uspgrlimlem4  48345  grlimprclnbgredg  48351  grlimgredgex  48354  grlimgrtrilem2  48356  grlictr  48369  clnbgr3stgrgrlim  48373  clnbgr3stgrgrlic  48374  1hegrlfgr  48486  funcringcsetcALTV2lem8  48651  funcringcsetclem8ALTV  48674  itcovalendof  49023  uptrlem1  49563  uptr2  49574  swapf2f1oaALT  49631  swapfcoa  49634  swapffunc  49635  fucoppc  49763  thincciso  49806  thinccisod  49807  lmdran  50024  cmdlan  50025  amgmwlem  50155