Theorem f1of 6822

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

Syntax hints:   → wi 4  ⟶wf 6534  –1-1→wf1 6535  –1-1-onto→wf1o 6537

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 210  df-an 401  df-f1 6543  df-f1o 6545

This theorem is referenced by:  f1ofn  6823  f1ompt  7108  f1oresrab  7125  fsn  7133  fsnunf  7185  f1ounsn  7272  f1ocnvfv1  7276  f1ocnvfv2  7277  fsnex  7283  f1ocnvdm  7285  fcof1oinvd  7293  fveqf1o  7302  isocnv  7330  isocnv3  7332  isores2  7333  isotr  7336  isofr2  7344  isopolem  7345  isosolem  7347  f1oiso2  7352  weniso  7354  f1ofveu  7406  f1oexrnex  7925  f1oabexg  7939  wemoiso  7971  mptcnfimad  7984  suppsnop  8175  smoiso  8350  mapsnd  8885  ralxpmap  8895  f1oen2g  8966  en1  9022  enfixsn  9075  mapen  9130  ac6sfi  9245  domunfican  9282  fiint  9287  mapfienlem1  9366  mapfienlem2  9367  mapfienlem3  9368  mapfien  9369  supisoex  9436  supiso  9437  ordiso2  9478  unxpwdom2  9551  cantnfle  9641  cantnfp1lem3  9650  cantnflem1b  9656  cantnflem1d  9658  cantnflem1  9659  cnfcomlem  9669  cnfcom  9670  cnfcom2lem  9671  cnfcom2  9672  cnfcom3lem  9673  cnfcom3  9674  cnfcom3clem  9675  djuin  9905  infxpenlem  9998  infxpenc  10003  infxpenc2lem2  10005  fseqenlem1  10009  acndom  10036  acndom2  10039  infpwfien  10047  iunfictbso  10099  infmap2  10201  ackbij2lem2  10223  infpssrlem3  10290  infpssrlem4  10291  fin23lem30  10327  isf32lem6  10343  isf32lem7  10344  isf32lem8  10345  enfin1ai  10369  axcc3  10423  axcclem  10442  ttukeylem7  10500  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem8  10624  canthp1lem2  10639  canthp1  10640  pwfseqlem4a  10647  pwfseqlem5  10649  axdc4uzlem  14021  seqf1olem1  14079  seqf1olem2  14080  seqf1o  14081  hashkf  14370  hasheqf1oi  14389  hasheqf1od  14391  hashcl  14394  hashgadd  14415  hashfacen  14493  hashf1lem1  14494  fz1isolem  14500  seqcoll  14503  seqcoll2  14504  cnrecnv  15218  sumeq2ii  15746  summolem3  15767  summolem2a  15768  fsum  15773  fsumf1o  15776  fsumss  15778  fsumcl2lem  15784  fsumadd  15793  fsummulc2  15837  fsumrelem  15861  ackbijnn  15884  prodeq2ii  15967  prodmolem3  15989  prodmolem2a  15990  fprod  15997  fprodf1o  16002  fprodss  16004  fprodser  16005  fprodcl2lem  16006  fprodmul  16016  fproddiv  16017  fprodn0  16035  fproddvdsd  16394  sadcaddlem  16516  sadadd2lem  16518  sadadd3  16520  sadaddlem  16525  sadasslem  16529  sadeq  16531  phimullem  16839  eulerthlem1  16841  eulerthlem2  16842  unbenlem  16969  vdwlem8  17049  0ram  17081  wunndx  17256  xpsaddlem  17628  xpsvsca  17632  xpsle  17634  idfucl  17939  setccatid  18142  setcinv  18148  catcisolem  18168  estrccatid  18189  funcestrcsetclem7  18203  funcestrcsetclem8  18204  funcsetcestrclem7  18218  funcsetcestrclem8  18219  yonffthlem  18339  gsumpropd2lem  18738  mgmhmf1o  18759  idmgmhm  18760  idmhm  18854  mhmf1o  18855  gsumws1  18898  ielefmnd  18947  idghm  19302  ghmf1o  19319  symgbas  19443  elsymgbas  19445  symgbasf  19447  symgbasfi  19450  symg1bas  19462  symggrp  19471  lactghmga  19476  symgfixf1  19508  f1omvdmvd  19514  f1omvdconj  19517  f1omvdco2  19519  pmtrfconj  19537  symggen  19541  pmtrdifellem1  19547  pmtrdifellem2  19548  psgnunilem1  19564  gsumval3eu  19975  gsumval3lem1  19976  gsumval3  19978  gsumzf1o  19983  gsumconst  20005  gsumsub  20019  gsumcom2  20046  dprdfsub  20094  dprdf1o  20105  dprdsn  20109  ablfaclem2  20159  rngisomfv1  20548  rngisom1  20549  rngisomring1  20551  fidomndrnglem  20857  srngcl  20933  lmhmf1o  21148  gsumfsum  21565  zntoslem  21687  islinds2  21944  lindsmm  21959  psrass1lem  22064  psrnegcl  22085  psrlinv  22086  coe1f2  22350  coe1add  22406  evls1rhmlem  22462  evl1sca  22475  pf1ind  22496  mat1dimelbas  22609  mat1f  22620  mdetleib2  22726  mdetrsca  22741  mdetralt  22746  mdetunilem7  22756  mdetunilem9  22758  ssidcn  23393  hmphdis  23934  indishmph  23936  cmphaushmeo  23938  ordthmeolem  23939  txhmeo  23941  qtopf1  23954  ufldom  24100  symgtgp  24244  tsmsf1o  24283  iducn  24420  imasdsf1olem  24511  xpsdsval  24519  imasf1obl  24626  icchmeo  25081  iccpnfcnv  25084  xrhmeo  25086  cnheiborlem  25094  ovolctb  25630  ovoliunlem1  25642  ovoliunlem2  25643  iunmbl2  25697  dyadmbl  25740  vitalilem2  25749  vitalilem3  25750  vitalilem4  25751  vitalilem5  25752  mbfid  25775  dvid  26058  dvexp  26093  dvcnvlem  26116  dvcnv  26117  dvcnvrelem2  26158  dvcnvre  26159  efcvx  26590  reefgim  26591  efif1olem4  26688  eff1olem  26691  logrncl  26710  relogcl  26718  dvrelog  26780  relogcn  26781  logcn  26790  logf1o2  26793  dvlog  26794  dvlog2  26796  advlog  26797  advlogexp  26798  logtayl  26803  logccv  26806  dvcxp1  26883  loglesqrt  26904  asinrebnd  27044  dvatan  27078  efrlim  27112  amgmlem  27132  lgamcvg2  27197  wilthlem2  27211  wilthlem3  27212  sqff1o  27324  lgsqrlem4  27491  logdivsum  27675  log2sumbnd  27686  isismt  28781  motcl  28786  motco  28787  cnvmot  28788  motgrp  28790  motcgrg  28791  f1otrg  29198  f1otrge  29199  axlowdimlem10  29279  axcontlem5  29296  axcontlem10  29301  uspgriedgedg  29504  upgrres1  29641  umgrres1  29642  upgriseupth  30536  pliguhgr  30816  dmadjrn  32225  unopnorm  32247  unopadj  32249  unoplin  32250  counop  32251  idcnop  32311  idhmop  32312  unopbd  32345  bracnln  32439  cnvbraval  32440  leopnmid  32468  nmopleid  32469  hmopidmch  32483  hmopidmpj  32484  disjrdx  32914  fmptco1f1o  32956  isoun  33025  padct  33041  fcobij  33043  fcobijfs  33044  fcobijfs2  33045  wrdpmcl  33236  ccatws1f1o  33249  ccatws1f1olast  33250  mndlactf1o  33328  mndractf1o  33329  abliso  33333  symgfcoeu  33380  symgcom  33381  pmtrcnel  33387  pmtrcnel2  33388  pmtrcnelor  33389  wrdpmtrlast  33391  cycpmco2f1  33422  cycpmco2rn  33423  cycpmco2lem2  33425  cycpmco2lem3  33426  cycpmco2lem4  33427  cycpmco2lem5  33428  cycpmco2lem6  33429  cycpmco2lem7  33430  cycpmco2  33431  cycpmconjv  33440  cycpmconjslem1  33452  cycpmconjslem2  33453  cycpmconjs  33454  islinds5  33660  ellspds  33661  1arithidomlem1  33803  1arithidomlem2  33804  1arithidom  33805  0mplrim  33882  selvply1rhmlemb  33887  mplvrpmlem  33911  mplvrpmfgalem  33912  mplvrpmmhm  33914  mplvrpmrhm  33915  esplyfval0  33932  esplylem  33934  esplympl  33935  esplymhp  33936  esplyfv1  33937  esplyfv  33938  esplysply  33939  esplyfval3  33940  vieta  33948  tpr2rico  34280  xrge0iifmhm  34307  xrge0pluscn  34308  rrhre  34389  esumf1o  34418  volmeas  34599  eulerpartgbij  34740  eulerpartlemmf  34743  eulerpartlemgvv  34744  eulerpartlemgf  34747  eulerpartlemgs2  34748  eulerpartlemn  34749  ballotlemsima  34884  reprpmtf1o  34991  logdivsqrle  35015  hgt750lemg  35019  vonf1owevOLD  35572  deranglem  35636  derangsn  35640  derangenlem  35641  subfacp1lem4  35653  subfacp1lem5  35654  subfacp1lem6  35655  cvmfolem  35749  cvmliftlem6  35760  poimirlem1  38250  poimirlem2  38251  poimirlem3  38252  poimirlem4  38253  poimirlem6  38255  poimirlem7  38256  poimirlem9  38258  poimirlem11  38260  poimirlem12  38261  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem20  38269  poimirlem22  38271  poimirlem26  38275  poimirlem27  38276  poimirlem28  38277  poimirlem32  38281  mblfinlem2  38287  dvasin  38333  f1ocan1fv  38355  metf1o  38384  ismtyval  38429  isismty  38430  ismtyima  38432  ismtyhmeolem  38433  ismtybndlem  38435  ismrer1  38467  reheibor  38468  grposnOLD  38511  rngoisocnv  38610  lflnegl  39828  lautset  40834  islaut  40835  lautcl  40839  lautco  40849  pautsetN  40850  ispautN  40851  ldilco  40868  ltrncoidN  40880  ltrncoval  40897  trlcoabs2N  41474  trlcoat  41475  trlcone  41480  cdlemg47a  41486  cdlemg46  41487  cdlemg47  41488  trljco  41492  tgrpgrplem  41501  tendoidcl  41521  tendo0co2  41540  tendo0pl  41543  cdlemi2  41571  cdlemk2  41584  cdlemk4  41586  cdlemk8  41590  cdlemkid2  41676  cdlemk45  41699  cdlemk53b  41708  cdlemk53  41709  cdlemk55a  41711  erng1r  41747  tendocnv  41773  dvalveclem  41777  dva0g  41779  dvhgrp  41859  dvh0g  41863  dvhopN  41868  cdlemn3  41949  cdlemn8  41956  cdlemn9  41957  dihordlem7b  41967  dihopelvalcpre  42000  dihmeetlem1N  42042  dihglblem5apreN  42043  lcfrlem13  42307  hvmapclN  42516  hvmapcl2  42518  dvrelog2  42809  dvrelog3  42810  sticksstones3  42893  sticksstones17  42908  sticksstones18  42909  sticksstones19  42910  readvrec2  43100  readvrec  43101  mapfzcons  43427  mzpresrename  43461  diophrw  43470  eldioph2  43473  diophren  43520  kelac1  43770  imasgim  43807  lnrfg  43826  nvocnvb  44128  brco2f1o  44738  brco3f1o  44739  clsneikex  44812  clsneinex  44813  clsneiel1  44814  neicvgmex  44823  neicvgel1  44825  dssmapntrcls  44834  stoweidlem27  46721  stoweidlem31  46725  stoweidlem39  46733  fourierdlem20  46821  fourierdlem50  46850  fourierdlem52  46852  fourierdlem54  46854  fourierdlem64  46864  fourierdlem76  46876  fourierdlem102  46902  fourierdlem114  46914  sge0f1o  47076  nnfoctbdjlem  47149  isomenndlem  47224  ovnsubaddlem1  47264  3f1oss1  47789  reuf1odnf  47821  reuf1od  47822  f1oresf1o2  48005  fundcmpsurbijinjpreimafv  48133  fundcmpsurinjimaid  48137  grimfn  48621  isgrim  48624  grimuhgr  48629  grimco  48631  uhgrimedgi  48632  isuspgrim0lem  48635  isuspgrim0  48636  isuspgrim  48638  upgrimwlklem4  48642  gricushgr  48659  isubgrgrim  48671  uhgrimisgrgriclem  48672  uhgrimisgrgric  48673  clnbgrgrim  48676  grimedg  48677  grtriclwlk3  48687  isubgr3stgrlem3  48710  isubgr3stgrlem4  48711  isubgr3stgrlem6  48713  isubgr3stgrlem7  48714  isubgr3stgrlem8  48715  isubgr3stgrlem9  48716  grlimfn  48721  isgrlim  48724  uspgrlimlem1  48730  uspgrlimlem2  48731  uspgrlimlem3  48732  uspgrlimlem4  48733  grlimprclnbgredg  48739  grlimgredgex  48742  grlimgrtrilem2  48744  grlictr  48757  clnbgr3stgrgrlim  48761  clnbgr3stgrgrlic  48762  1hegrlfgr  48874  funcringcsetcALTV2lem8  49039  funcringcsetclem8ALTV  49062  itcovalendof  49426  uptrlem1  49965  uptr2  49976  swapf2f1oaALT  50033  swapfcoa  50036  swapffunc  50037  fucoppc  50165  thincciso  50208  thinccisod  50209  lmdran  50426  cmdlan  50427  amgmwlem  50579