Theorem f1of 6821

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

This proof depends on syntax axioms:   → wi 4  ⟶wf 6533  –1-1→wf1 6534  –1-1-onto→wf1o 6536

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 6542  df-f1o 6544

This theorem is used by:  f1ofn  6822  f1ompt  7108  f1oresrab  7125  fsn  7133  fsnunf  7187  f1ounsn  7277  f1ocnvfv1  7281  f1ocnvfv2  7282  fsnex  7288  f1ocnvdm  7290  fcof1oinvd  7298  fveqf1o  7307  isocnv  7335  isocnv3  7337  isores2  7338  isotr  7341  isofr2  7349  isopolem  7350  isosolem  7352  f1oiso2  7357  weniso  7361  f1ofveu  7411  f1oexrnex  7928  f1oabexg  7942  wemoiso  7974  mptcnfimad  7987  suppsnop  8180  smoiso  8355  mapsnd  8897  ralxpmap  8907  f1oen2g  8978  en1  9034  enfixsn  9088  mapen  9143  ac6sfi  9258  domunfican  9295  fiint  9300  mapfienlem1  9379  mapfienlem2  9380  mapfienlem3  9381  mapfien  9382  supisoex  9449  supiso  9450  ordiso2  9491  unxpwdom2  9564  cantnfle  9654  cantnfp1lem3  9663  cantnflem1b  9669  cantnflem1d  9671  cantnflem1  9672  cnfcomlem  9682  cnfcom  9683  cnfcom2lem  9684  cnfcom2  9685  cnfcom3lem  9686  cnfcom3  9687  cnfcom3clem  9688  djuin  9927  infxpenlem  10020  infxpenc  10025  infxpenc2lem2  10027  fseqenlem1  10031  acndom  10058  acndom2  10061  infpwfien  10069  iunfictbso  10121  infmap2  10223  ackbij2lem2  10245  infpssrlem3  10311  infpssrlem4  10312  fin23lem30  10348  isf32lem6  10364  isf32lem7  10365  isf32lem8  10366  enfin1ai  10390  axcc3  10444  axcclem  10463  ttukeylem7  10521  fpwwe2lem5  10648  fpwwe2lem6  10649  fpwwe2lem8  10651  canthp1lem2  10666  canthp1  10667  pwfseqlem4a  10674  pwfseqlem5  10676  axdc4uzlem  14051  seqf1olem1  14109  seqf1olem2  14110  seqf1o  14111  hashkf  14400  hasheqf1oi  14419  hasheqf1od  14421  hashcl  14424  hashgadd  14445  hashfacen  14523  hashf1lem1  14524  fz1isolem  14530  seqcoll  14533  seqcoll2  14534  cnrecnv  15256  sumeq2ii  15784  summolem3  15804  summolem2a  15805  fsum  15810  fsumf1o  15813  fsumss  15815  fsumcl2lem  15821  fsumadd  15830  fsummulc2  15874  fsumrelem  15898  ackbijnn  15921  prodeq2ii  16004  prodmolem3  16026  prodmolem2a  16027  fprod  16034  fprodf1o  16039  fprodss  16041  fprodser  16042  fprodcl2lem  16043  fprodmul  16053  fproddiv  16054  fprodn0  16072  fproddvdsd  16431  sadcaddlem  16553  sadadd2lem  16555  sadadd3  16557  sadaddlem  16562  sadasslem  16566  sadeq  16568  phimullem  16876  eulerthlem1  16878  eulerthlem2  16879  unbenlem  17006  vdwlem8  17086  0ram  17118  wunndx  17293  xpsaddlem  17665  xpsvsca  17669  xpsle  17671  idfucl  17976  setccatid  18179  setcinv  18185  catcisolem  18205  estrccatid  18226  funcestrcsetclem7  18240  funcestrcsetclem8  18241  funcsetcestrclem7  18255  funcsetcestrclem8  18256  yonffthlem  18376  gsumpropd2lem  18787  mgmhmf1o  18808  idmgmhm  18809  idmhm  18909  mhmf1o  18910  gsumws1  18953  ielefmnd  19002  idghm  19364  ghmf1o  19381  symgbas  19505  elsymgbas  19507  symgbasf  19509  symgbasfi  19512  symg1bas  19524  symggrp  19533  lactghmga  19538  symgfixf1  19570  f1omvdmvd  19576  f1omvdconj  19579  f1omvdco2  19581  pmtrfconj  19599  symggen  19603  pmtrdifellem1  19609  pmtrdifellem2  19610  psgnunilem1  19626  gsumval3eu  20037  gsumval3lem1  20038  gsumval3  20040  gsumzf1o  20045  gsumconst  20067  gsumsub  20081  gsumcom2  20108  dprdfsub  20156  dprdf1o  20167  dprdsn  20171  ablfaclem2  20221  rngisomfv1  20612  rngisom1  20613  rngisomring1  20615  fidomndrnglem  20945  srngcl  21021  lmhmf1o  21236  gsumfsum  21653  zntoslem  21775  islinds2  22032  lindsmm  22047  psrass1lem  22154  psrnegcl  22175  psrlinv  22176  coe1f2  22440  coe1add  22496  evls1rhmlem  22552  evl1sca  22565  pf1ind  22586  mat1dimelbas  22699  mat1f  22710  mdetleib2  22816  mdetrsca  22831  mdetralt  22836  mdetunilem7  22846  mdetunilem9  22848  ssidcn  23486  hmphdis  24028  indishmph  24030  cmphaushmeo  24032  ordthmeolem  24033  txhmeo  24035  qtopf1  24048  ufldom  24194  symgtgp  24338  tsmsf1o  24377  iducn  24514  imasdsf1olem  24605  xpsdsval  24613  imasf1obl  24720  icchmeo  25175  iccpnfcnv  25178  xrhmeo  25180  cnheiborlem  25188  ovolctb  25724  ovoliunlem1  25736  ovoliunlem2  25737  iunmbl2  25791  dyadmbl  25834  vitalilem2  25843  vitalilem3  25844  vitalilem4  25845  vitalilem5  25846  mbfid  25869  dvid  26152  dvexp  26187  dvcnvlem  26210  dvcnv  26211  dvcnvrelem2  26252  dvcnvre  26253  efcvx  26692  reefgim  26693  efif1olem4  26790  eff1olem  26793  logrncl  26812  relogcl  26820  dvrelog  26882  relogcn  26883  logcn  26892  logf1o2  26895  dvlog  26896  dvlog2  26898  advlog  26899  advlogexp  26900  logtayl  26905  logccv  26908  dvcxp1  26985  loglesqrt  27006  asinrebnd  27146  dvatan  27180  efrlim  27214  amgmlem  27234  lgamcvg2  27299  wilthlem2  27313  wilthlem3  27314  sqff1o  27426  lgsqrlem4  27593  logdivsum  27777  log2sumbnd  27788  isismt  28884  motcl  28889  motco  28890  cnvmot  28891  motgrp  28893  motcgrg  28894  f1otrg  29335  f1otrge  29336  axlowdimlem10  29416  axcontlem5  29433  axcontlem10  29438  uspgriedgedg  29644  upgrres1  29781  umgrres1  29782  upgriseupth  30695  pliguhgr  30975  dmadjrn  32384  unopnorm  32406  unopadj  32408  unoplin  32409  counop  32410  idcnop  32470  idhmop  32471  unopbd  32504  bracnln  32598  cnvbraval  32599  leopnmid  32627  nmopleid  32628  hmopidmch  32642  hmopidmpj  32643  disjrdx  33072  fmptco1f1o  33114  isoun  33182  padct  33197  fcobij  33199  fcobijfs  33200  fcobijfs2  33201  wrdpmcl  33392  ccatws1f1o  33401  ccatws1f1olast  33402  mndlactf1o  33478  mndractf1o  33479  abliso  33483  symgfcoeu  33530  symgcom  33531  pmtrcnel  33537  pmtrcnel2  33538  pmtrcnelor  33539  wrdpmtrlast  33541  cycpmco2f1  33572  cycpmco2rn  33573  cycpmco2lem2  33575  cycpmco2lem3  33576  cycpmco2lem4  33577  cycpmco2lem5  33578  cycpmco2lem6  33579  cycpmco2lem7  33580  cycpmco2  33581  cycpmconjv  33590  cycpmconjslem1  33602  cycpmconjslem2  33603  cycpmconjs  33604  islinds5  33810  ellspds  33811  1arithidomlem1  33953  1arithidomlem2  33954  1arithidom  33955  0mplrim  34032  selvply1rhmlemb  34037  mplvrpmlem  34061  mplvrpmfgalem  34062  mplvrpmmhm  34064  mplvrpmrhm  34065  esplyfval0  34082  esplylem  34084  esplympl  34085  esplymhp  34086  esplyfv1  34087  esplyfv  34088  esplysply  34089  esplyfval3  34090  vieta  34098  tpr2rico  34430  xrge0iifmhm  34457  xrge0pluscn  34458  rrhre  34539  esumf1o  34568  volmeas  34750  eulerpartgbij  34891  eulerpartlemmf  34894  eulerpartlemgvv  34895  eulerpartlemgf  34898  eulerpartlemgs2  34899  eulerpartlemn  34900  ballotlemsima  35035  reprpmtf1o  35142  logdivsqrle  35166  hgt750lemg  35170  vonf1owevOLD  35715  deranglem  35753  derangsn  35757  derangenlem  35758  subfacp1lem4  35770  subfacp1lem5  35771  subfacp1lem6  35772  cvmfolem  35866  cvmliftlem6  35877  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem9  38386  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  poimirlem32  38409  mblfinlem2  38415  dvasin  38461  f1ocan1fv  38484  metf1o  38513  ismtyval  38558  isismty  38559  ismtyima  38561  ismtyhmeolem  38562  ismtybndlem  38564  ismrer1  38596  reheibor  38597  grposnOLD  38640  rngoisocnv  38739  lflnegl  39957  lautset  40963  islaut  40964  lautcl  40968  lautco  40978  pautsetN  40979  ispautN  40980  ldilco  40997  ltrncoidN  41009  ltrncoval  41026  trlcoabs2N  41603  trlcoat  41604  trlcone  41609  cdlemg47a  41615  cdlemg46  41616  cdlemg47  41617  trljco  41621  tgrpgrplem  41630  tendoidcl  41650  tendo0co2  41669  tendo0pl  41672  cdlemi2  41700  cdlemk2  41713  cdlemk4  41715  cdlemk8  41719  cdlemkid2  41805  cdlemk45  41828  cdlemk53b  41837  cdlemk53  41838  cdlemk55a  41840  erng1r  41876  tendocnv  41902  dvalveclem  41906  dva0g  41908  dvhgrp  41988  dvh0g  41992  dvhopN  41997  cdlemn3  42078  cdlemn8  42085  cdlemn9  42086  dihordlem7b  42096  dihopelvalcpre  42129  dihmeetlem1N  42171  dihglblem5apreN  42172  lcfrlem13  42436  hvmapclN  42645  hvmapcl2  42647  dvrelog2  42938  dvrelog3  42939  sticksstones3  43022  sticksstones17  43037  sticksstones18  43038  sticksstones19  43039  readvrec2  43244  readvrec  43245  mapfzcons  43569  mzpresrename  43603  diophrw  43612  eldioph2  43615  diophren  43662  kelac1  43912  imasgim  43949  lnrfg  43968  nvocnvb  44270  brco2f1o  44880  brco3f1o  44881  clsneikex  44954  clsneinex  44955  clsneiel1  44956  neicvgmex  44965  neicvgel1  44967  dssmapntrcls  44976  stoweidlem27  46863  stoweidlem31  46867  stoweidlem39  46875  fourierdlem20  46963  fourierdlem50  46992  fourierdlem52  46994  fourierdlem54  46996  fourierdlem64  47006  fourierdlem76  47018  fourierdlem102  47044  fourierdlem114  47056  sge0f1o  47218  nnfoctbdjlem  47291  isomenndlem  47366  ovnsubaddlem1  47406  3f1oss1  47971  reuf1odnf  48003  reuf1od  48004  f1oresf1o2  48187  fundcmpsurbijinjpreimafv  48315  fundcmpsurinjimaid  48319  grimfn  48803  isgrim  48806  grimuhgr  48811  grimco  48813  uhgrimedgi  48814  isuspgrim0lem  48817  isuspgrim0  48818  isuspgrim  48820  upgrimwlklem4  48824  gricushgr  48841  isubgrgrim  48853  uhgrimisgrgriclem  48854  uhgrimisgrgric  48855  clnbgrgrim  48858  grimedg  48859  grtriclwlk3  48869  isubgr3stgrlem3  48892  isubgr3stgrlem4  48893  isubgr3stgrlem6  48895  isubgr3stgrlem7  48896  isubgr3stgrlem8  48897  isubgr3stgrlem9  48898  grlimfn  48903  isgrlim  48906  uspgrlimlem1  48912  uspgrlimlem2  48913  uspgrlimlem3  48914  uspgrlimlem4  48915  grlimprclnbgredg  48921  grlimgredgex  48924  grlimgrtrilem2  48926  grlictr  48939  clnbgr3stgrgrlim  48943  clnbgr3stgrgrlic  48944  1hegrlfgr  49056  funcringcsetcALTV2lem8  49220  funcringcsetclem8ALTV  49243  itcovalendof  49607  uptrlem1  50144  uptr2  50155  swapf2f1oaALT  50212  swapfcoa  50215  swapffunc  50216  fucoppc  50344  thincciso  50387  thinccisod  50388  lmdran  50605  cmdlan  50606  amgmwlem  50828