Theorem f1of 6828

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

Syntax hints:   → wi 4  ⟶wf 6537  –1-1→wf1 6538  –1-1-onto→wf1o 6540

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 6546  df-f1o 6548

This theorem is referenced by:  f1ofn  6829  f1ompt  7111  f1oresrab  7127  fsn  7135  fsnunf  7187  f1ounsn  7274  f1ocnvfv1  7278  f1ocnvfv2  7279  fsnex  7285  f1ocnvdm  7287  fcof1oinvd  7295  fveqf1o  7304  isocnv  7332  isocnv3  7334  isores2  7335  isotr  7338  isofr2  7346  isopolem  7347  isosolem  7349  f1oiso2  7354  weniso  7356  f1ofveu  7407  f1oexrnex  7931  f1oabexg  7946  f1oabexgOLD  7947  wemoiso  7980  mptcnfimad  7993  suppsnop  8185  smoiso  8384  mapsnd  8908  ralxpmap  8918  f1oen2g  8991  en1  9046  enfixsn  9103  mapen  9163  ac6sfi  9302  domunfican  9343  fiint  9348  fiintOLD  9349  mapfienlem1  9427  mapfienlem2  9428  mapfienlem3  9429  mapfien  9430  supisoex  9496  supiso  9497  ordiso2  9537  unxpwdom2  9610  cantnfle  9693  cantnfp1lem3  9702  cantnflem1b  9708  cantnflem1d  9710  cantnflem1  9711  cnfcomlem  9721  cnfcom  9722  cnfcom2lem  9723  cnfcom2  9724  cnfcom3lem  9725  cnfcom3  9726  cnfcom3clem  9727  djuin  9940  infxpenlem  10035  infxpenc  10040  infxpenc2lem2  10042  fseqenlem1  10046  acndom  10073  acndom2  10076  infpwfien  10084  iunfictbso  10136  infmap2  10239  ackbij2lem2  10261  infpssrlem3  10327  infpssrlem4  10328  fin23lem30  10364  isf32lem6  10380  isf32lem7  10381  isf32lem8  10382  enfin1ai  10406  axcc3  10460  axcclem  10479  ttukeylem7  10537  fpwwe2lem5  10657  fpwwe2lem6  10658  fpwwe2lem8  10660  canthp1lem2  10675  canthp1  10676  pwfseqlem4a  10683  pwfseqlem5  10685  axdc4uzlem  14006  seqf1olem1  14064  seqf1olem2  14065  seqf1o  14066  hashkf  14354  hasheqf1oi  14373  hasheqf1od  14375  hashcl  14378  hashgadd  14399  hashfacen  14476  hashf1lem1  14477  fz1isolem  14483  seqcoll  14486  seqcoll2  14487  cnrecnv  15187  sumeq2ii  15712  summolem3  15733  summolem2a  15734  fsum  15739  fsumf1o  15742  fsumss  15744  fsumcl2lem  15750  fsumadd  15759  fsummulc2  15803  fsumrelem  15826  ackbijnn  15847  prodeq2ii  15930  prodmolem3  15952  prodmolem2a  15953  fprod  15960  fprodf1o  15965  fprodss  15967  fprodser  15968  fprodcl2lem  15969  fprodmul  15979  fproddiv  15980  fprodn0  15998  fproddvdsd  16355  sadcaddlem  16477  sadadd2lem  16479  sadadd3  16481  sadaddlem  16486  sadasslem  16490  sadeq  16492  phimullem  16799  eulerthlem1  16801  eulerthlem2  16802  unbenlem  16929  vdwlem8  17009  0ram  17041  wunndx  17215  xpsaddlem  17590  xpsvsca  17594  xpsle  17596  idfucl  17898  setccatid  18101  setcinv  18107  catcisolem  18127  estrccatid  18148  funcestrcsetclem7  18162  funcestrcsetclem8  18163  funcsetcestrclem7  18177  funcsetcestrclem8  18178  yonffthlem  18298  gsumpropd2lem  18662  mgmhmf1o  18683  idmgmhm  18684  idmhm  18778  mhmf1o  18779  gsumws1  18821  ielefmnd  18870  idghm  19219  ghmf1o  19236  symgbas  19358  elsymgbas  19360  symgbasf  19362  symgbasfi  19365  symg1bas  19377  symggrp  19387  lactghmga  19392  symgfixf1  19424  f1omvdmvd  19430  f1omvdconj  19433  f1omvdco2  19435  pmtrfconj  19453  symggen  19457  pmtrdifellem1  19463  pmtrdifellem2  19464  psgnunilem1  19480  gsumval3eu  19891  gsumval3lem1  19892  gsumval3  19894  gsumzf1o  19899  gsumconst  19921  gsumsub  19935  gsumcom2  19962  dprdfsub  20010  dprdf1o  20021  dprdsn  20025  ablfaclem2  20075  rngisomfv1  20434  rngisom1  20435  rngisomring1  20437  fidomndrnglem  20742  srngcl  20819  lmhmf1o  21014  gsumfsum  21415  zntoslem  21530  islinds2  21788  lindsmm  21803  psrass1lem  21907  psrnegcl  21929  psrlinv  21930  coe1f2  22160  coe1add  22216  evls1rhmlem  22274  evl1sca  22287  pf1ind  22308  mat1dimelbas  22426  mat1f  22437  mdetleib2  22543  mdetrsca  22558  mdetralt  22563  mdetunilem7  22573  mdetunilem9  22575  ssidcn  23210  hmphdis  23751  indishmph  23753  cmphaushmeo  23755  ordthmeolem  23756  txhmeo  23758  qtopf1  23771  ufldom  23917  symgtgp  24061  tsmsf1o  24100  iducn  24238  imasdsf1olem  24329  xpsdsval  24337  imasf1obl  24446  icchmeo  24908  icchmeoOLD  24909  iccpnfcnv  24912  xrhmeo  24914  cnheiborlem  24923  ovolctb  25462  ovoliunlem1  25474  ovoliunlem2  25475  iunmbl2  25529  dyadmbl  25572  vitalilem2  25581  vitalilem3  25582  vitalilem4  25583  vitalilem5  25584  mbfid  25607  dvid  25890  dvexp  25928  dvcnvlem  25951  dvcnv  25952  dvcnvrelem2  25994  dvcnvre  25995  efcvx  26430  reefgim  26431  efif1olem4  26524  eff1olem  26527  logrncl  26546  relogcl  26554  dvrelog  26616  relogcn  26617  logcn  26626  logf1o2  26629  dvlog  26630  dvlog2  26632  advlog  26633  advlogexp  26634  logtayl  26639  logccv  26642  dvcxp1  26719  loglesqrt  26741  asinrebnd  26881  dvatan  26915  efrlim  26949  efrlimOLD  26950  amgmlem  26970  lgamcvg2  27035  wilthlem2  27049  wilthlem3  27050  sqff1o  27162  lgsqrlem4  27330  logdivsum  27514  log2sumbnd  27525  isismt  28479  motcl  28484  motco  28485  cnvmot  28486  motgrp  28488  motcgrg  28489  f1otrg  28816  f1otrge  28817  axlowdimlem10  28897  axcontlem5  28914  axcontlem10  28919  uspgriedgedg  29122  upgrres1  29259  umgrres1  29260  upgriseupth  30155  pliguhgr  30434  dmadjrn  31843  unopnorm  31865  unopadj  31867  unoplin  31868  counop  31869  idcnop  31929  idhmop  31930  unopbd  31963  bracnln  32057  cnvbraval  32058  leopnmid  32086  nmopleid  32087  hmopidmch  32101  hmopidmpj  32102  disjrdx  32540  fmptco1f1o  32579  isoun  32647  padct  32667  fcobij  32669  fcobijfs  32670  wrdpmcl  32867  ccatws1f1o  32881  ccatws1f1olast  32882  mndlactf1o  32979  mndractf1o  32980  abliso  32985  symgfcoeu  33046  symgcom  33047  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  wrdpmtrlast  33057  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cycpmconjv  33106  cycpmconjslem1  33118  cycpmconjslem2  33119  cycpmconjs  33120  islinds5  33335  ellspds  33336  1arithidomlem1  33503  1arithidomlem2  33504  1arithidom  33505  tpr2rico  33886  xrge0iifmhm  33913  xrge0pluscn  33914  rrhre  33997  esumf1o  34026  volmeas  34207  eulerpartgbij  34349  eulerpartlemmf  34352  eulerpartlemgvv  34353  eulerpartlemgf  34356  eulerpartlemgs2  34357  eulerpartlemn  34358  ballotlemsima  34493  reprpmtf1o  34616  logdivsqrle  34640  hgt750lemg  34644  deranglem  35146  derangsn  35150  derangenlem  35151  subfacp1lem4  35163  subfacp1lem5  35164  subfacp1lem6  35165  cvmfolem  35259  cvmliftlem6  35270  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem9  37611  poimirlem11  37613  poimirlem12  37614  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem22  37624  poimirlem26  37628  poimirlem27  37629  poimirlem28  37630  poimirlem32  37634  mblfinlem2  37640  dvasin  37686  f1ocan1fv  37708  metf1o  37737  ismtyval  37782  isismty  37783  ismtyima  37785  ismtyhmeolem  37786  ismtybndlem  37788  ismrer1  37820  reheibor  37821  grposnOLD  37864  rngoisocnv  37963  lflnegl  39052  lautset  40059  islaut  40060  lautcl  40064  lautco  40074  pautsetN  40075  ispautN  40076  ldilco  40093  ltrncoidN  40105  ltrncoval  40122  trlcoabs2N  40699  trlcoat  40700  trlcone  40705  cdlemg47a  40711  cdlemg46  40712  cdlemg47  40713  trljco  40717  tgrpgrplem  40726  tendoidcl  40746  tendo0co2  40765  tendo0pl  40768  cdlemi2  40796  cdlemk2  40809  cdlemk4  40811  cdlemk8  40815  cdlemkid2  40901  cdlemk45  40924  cdlemk53b  40933  cdlemk53  40934  cdlemk55a  40936  erng1r  40972  tendocnv  40998  dvalveclem  41002  dva0g  41004  dvhgrp  41084  dvh0g  41088  dvhopN  41093  cdlemn3  41174  cdlemn8  41181  cdlemn9  41182  dihordlem7b  41192  dihopelvalcpre  41225  dihmeetlem1N  41267  dihglblem5apreN  41268  lcfrlem13  41532  hvmapclN  41741  hvmapcl2  41743  dvrelog2  42040  dvrelog3  42041  sticksstones3  42124  sticksstones17  42139  sticksstones18  42140  sticksstones19  42141  metakunt33  42213  readvrec2  42370  readvrec  42371  mapfzcons  42705  mzpresrename  42739  diophrw  42748  eldioph2  42751  diophren  42802  kelac1  43053  imasgim  43090  lnrfg  43109  nvocnvb  43412  brco2f1o  44022  brco3f1o  44023  clsneikex  44096  clsneinex  44097  clsneiel1  44098  neicvgmex  44107  neicvgel1  44109  dssmapntrcls  44118  stoweidlem27  46014  stoweidlem31  46018  stoweidlem39  46026  fourierdlem20  46114  fourierdlem50  46143  fourierdlem52  46145  fourierdlem54  46147  fourierdlem64  46157  fourierdlem76  46169  fourierdlem102  46195  fourierdlem114  46207  sge0f1o  46369  nnfoctbdjlem  46442  isomenndlem  46517  ovnsubaddlem1  46557  3f1oss1  47060  reuf1odnf  47092  reuf1od  47093  f1oresf1o2  47276  fundcmpsurbijinjpreimafv  47367  fundcmpsurinjimaid  47371  grimfn  47838  isgrim  47841  isuspgrim0lem  47844  isuspgrim0  47845  uspgrimprop  47846  isuspgrim  47848  grimuhgr  47851  grimco  47853  gricushgr  47859  isubgrgrim  47870  uhgrimisgrgriclem  47871  uhgrimisgrgric  47872  clnbgrgrim  47875  grimedg  47876  grtriclwlk3  47885  isubgr3stgrlem3  47908  isubgr3stgrlem4  47909  isubgr3stgrlem6  47911  isubgr3stgrlem7  47912  isubgr3stgrlem8  47913  isubgr3stgrlem9  47914  grlimfn  47919  isgrlim  47922  uspgrlimlem1  47928  uspgrlimlem2  47929  uspgrlimlem3  47930  uspgrlimlem4  47931  grlimgrtrilem2  47935  grlictr  47948  clnbgr3stgrgrlic  47952  1hegrlfgr  48021  funcringcsetcALTV2lem8  48186  funcringcsetclem8ALTV  48209  itcovalendof  48563  swapf2f1oaALT  49029  swapfcoa  49032  swapffunc  49033  thincciso  49154  thinccisod  49155  amgmwlem  49416