Theorem f1of 6865

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

Syntax hints:   → wi 4  ⟶wf 6572  –1-1→wf1 6573  –1-1-onto→wf1o 6575

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 6581  df-f1o 6583

This theorem is referenced by:  f1ofn  6866  f1ompt  7148  f1oresrab  7164  fsn  7172  fsnunf  7222  f1ocnvfv1  7315  f1ocnvfv2  7316  fsnex  7322  f1ocnvdm  7324  fcof1oinvd  7332  fveqf1o  7341  isocnv  7369  isocnv3  7371  isores2  7372  isotr  7375  isofr2  7383  isopolem  7384  isosolem  7386  f1oiso2  7391  weniso  7393  f1ofveu  7445  f1oexrnex  7970  f1oabexg  7983  f1oabexgOLD  7984  wemoiso  8017  mptcnfimad  8030  suppsnop  8222  smoiso  8421  mapsnd  8947  ralxpmap  8957  f1oen2g  9031  en1  9089  en1OLD  9090  enfixsn  9150  mapen  9210  ac6sfi  9351  domunfican  9392  fiint  9397  fiintOLD  9398  mapfienlem1  9477  mapfienlem2  9478  mapfienlem3  9479  mapfien  9480  supisoex  9546  supiso  9547  ordiso2  9587  unxpwdom2  9660  cantnfle  9743  cantnfp1lem3  9752  cantnflem1b  9758  cantnflem1d  9760  cantnflem1  9761  cnfcomlem  9771  cnfcom  9772  cnfcom2lem  9773  cnfcom2  9774  cnfcom3lem  9775  cnfcom3  9776  cnfcom3clem  9777  djuin  9990  infxpenlem  10085  infxpenc  10090  infxpenc2lem2  10092  fseqenlem1  10096  acndom  10123  acndom2  10126  infpwfien  10134  iunfictbso  10186  infmap2  10289  ackbij2lem2  10311  infpssrlem3  10377  infpssrlem4  10378  fin23lem30  10414  isf32lem6  10430  isf32lem7  10431  isf32lem8  10432  enfin1ai  10456  axcc3  10510  axcclem  10529  ttukeylem7  10587  fpwwe2lem5  10707  fpwwe2lem6  10708  fpwwe2lem8  10710  canthp1lem2  10725  canthp1  10726  pwfseqlem4a  10733  pwfseqlem5  10735  axdc4uzlem  14051  seqf1olem1  14109  seqf1olem2  14110  seqf1o  14111  hashkf  14398  hasheqf1oi  14417  hasheqf1od  14419  hashcl  14422  hashgadd  14443  hashfacen  14520  hashf1lem1  14521  fz1isolem  14527  seqcoll  14530  seqcoll2  14531  cnrecnv  15231  sumeq2ii  15758  summolem3  15779  summolem2a  15780  fsum  15785  fsumf1o  15788  fsumss  15790  fsumcl2lem  15796  fsumadd  15805  fsummulc2  15849  fsumrelem  15872  ackbijnn  15893  prodeq2ii  15976  prodmolem3  15998  prodmolem2a  15999  fprod  16006  fprodf1o  16011  fprodss  16013  fprodser  16014  fprodcl2lem  16015  fprodmul  16025  fproddiv  16026  fprodn0  16044  fproddvdsd  16401  sadcaddlem  16523  sadadd2lem  16525  sadadd3  16527  sadaddlem  16532  sadasslem  16536  sadeq  16538  phimullem  16846  eulerthlem1  16848  eulerthlem2  16849  unbenlem  16975  vdwlem8  17055  0ram  17087  wunndx  17262  xpsaddlem  17653  xpsvsca  17657  xpsle  17659  idfucl  17965  setccatid  18171  setcinv  18177  catcisolem  18197  estrccatid  18220  funcestrcsetclem7  18235  funcestrcsetclem8  18236  funcsetcestrclem7  18250  funcsetcestrclem8  18251  yonffthlem  18372  gsumpropd2lem  18737  mgmhmf1o  18758  idmgmhm  18759  idmhm  18850  mhmf1o  18851  gsumws1  18893  ielefmnd  18942  idghm  19291  ghmf1o  19308  symgbas  19433  elsymgbas  19435  symgbasf  19437  symgbasfi  19440  symg1bas  19452  symggrp  19462  lactghmga  19467  symgfixf1  19499  f1omvdmvd  19505  f1omvdconj  19508  f1omvdco2  19510  pmtrfconj  19528  symggen  19532  pmtrdifellem1  19538  pmtrdifellem2  19539  psgnunilem1  19555  gsumval3eu  19966  gsumval3lem1  19967  gsumval3  19969  gsumzf1o  19974  gsumconst  19996  gsumsub  20010  gsumcom2  20037  dprdfsub  20085  dprdf1o  20096  dprdsn  20100  ablfaclem2  20150  rngisomfv1  20511  rngisom1  20512  rngisomring1  20514  fidomndrnglem  20815  srngcl  20892  lmhmf1o  21088  gsumfsum  21495  zntoslem  21618  islinds2  21876  lindsmm  21891  psrass1lem  21995  psrnegcl  22017  psrlinv  22018  coe1f2  22252  coe1add  22308  evls1rhmlem  22366  evl1sca  22379  pf1ind  22400  mat1dimelbas  22518  mat1f  22529  mdetleib2  22635  mdetrsca  22650  mdetralt  22655  mdetunilem7  22665  mdetunilem9  22667  ssidcn  23304  hmphdis  23845  indishmph  23847  cmphaushmeo  23849  ordthmeolem  23850  txhmeo  23852  qtopf1  23865  ufldom  24011  symgtgp  24155  tsmsf1o  24194  iducn  24333  imasdsf1olem  24424  xpsdsval  24432  imasf1obl  24542  icchmeo  25010  icchmeoOLD  25011  iccpnfcnv  25014  xrhmeo  25016  cnheiborlem  25025  ovolctb  25564  ovoliunlem1  25576  ovoliunlem2  25577  iunmbl2  25631  dyadmbl  25674  vitalilem2  25683  vitalilem3  25684  vitalilem4  25685  vitalilem5  25686  mbfid  25709  dvid  25993  dvexp  26031  dvcnvlem  26054  dvcnv  26055  dvcnvrelem2  26097  dvcnvre  26098  efcvx  26531  reefgim  26532  efif1olem4  26625  eff1olem  26628  logrncl  26647  relogcl  26655  dvrelog  26717  relogcn  26718  logcn  26727  logf1o2  26730  dvlog  26731  dvlog2  26733  advlog  26734  advlogexp  26735  logtayl  26740  logccv  26743  dvcxp1  26820  loglesqrt  26842  asinrebnd  26982  dvatan  27016  efrlim  27050  efrlimOLD  27051  amgmlem  27071  lgamcvg2  27136  wilthlem2  27150  wilthlem3  27151  sqff1o  27263  lgsqrlem4  27431  logdivsum  27615  log2sumbnd  27626  isismt  28580  motcl  28585  motco  28586  cnvmot  28587  motgrp  28589  motcgrg  28590  f1otrg  28917  f1otrge  28918  axlowdimlem10  29004  axcontlem5  29021  axcontlem10  29026  uspgriedgedg  29231  upgrres1  29368  umgrres1  29369  upgriseupth  30259  pliguhgr  30538  dmadjrn  31947  unopnorm  31969  unopadj  31971  unoplin  31972  counop  31973  idcnop  32033  idhmop  32034  unopbd  32067  bracnln  32161  cnvbraval  32162  leopnmid  32190  nmopleid  32191  hmopidmch  32205  hmopidmpj  32206  disjrdx  32633  fmptco1f1o  32672  isoun  32733  padct  32753  fcobij  32756  fcobijfs  32757  wrdpmcl  32924  ccatws1f1o  32938  ccatws1f1olast  32939  mndlactf1o  33036  mndractf1o  33037  abliso  33042  symgfcoeu  33095  symgcom  33096  pmtrcnel  33102  pmtrcnel2  33103  pmtrcnelor  33104  wrdpmtrlast  33106  cycpmco2f1  33137  cycpmco2rn  33138  cycpmco2lem2  33140  cycpmco2lem3  33141  cycpmco2lem4  33142  cycpmco2lem5  33143  cycpmco2lem6  33144  cycpmco2lem7  33145  cycpmco2  33146  cycpmconjv  33155  cycpmconjslem1  33167  cycpmconjslem2  33168  cycpmconjs  33169  islinds5  33380  ellspds  33381  1arithidomlem1  33548  1arithidomlem2  33549  1arithidom  33550  tpr2rico  33878  xrge0iifmhm  33905  xrge0pluscn  33906  rrhre  33987  esumf1o  34034  volmeas  34215  eulerpartgbij  34357  eulerpartlemmf  34360  eulerpartlemgvv  34361  eulerpartlemgf  34364  eulerpartlemgs2  34365  eulerpartlemn  34366  ballotlemsima  34500  reprpmtf1o  34623  logdivsqrle  34647  hgt750lemg  34651  deranglem  35154  derangsn  35158  derangenlem  35159  subfacp1lem4  35171  subfacp1lem5  35172  subfacp1lem6  35173  cvmfolem  35267  cvmliftlem6  35278  poimirlem1  37601  poimirlem2  37602  poimirlem3  37603  poimirlem4  37604  poimirlem6  37606  poimirlem7  37607  poimirlem9  37609  poimirlem11  37611  poimirlem12  37612  poimirlem16  37616  poimirlem17  37617  poimirlem19  37619  poimirlem20  37620  poimirlem22  37622  poimirlem26  37626  poimirlem27  37627  poimirlem28  37628  poimirlem32  37632  mblfinlem2  37638  dvasin  37684  f1ocan1fv  37706  metf1o  37735  ismtyval  37780  isismty  37781  ismtyima  37783  ismtyhmeolem  37784  ismtybndlem  37786  ismrer1  37818  reheibor  37819  grposnOLD  37862  rngoisocnv  37961  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  mapfzcons  42691  mzpresrename  42725  diophrw  42734  eldioph2  42737  diophren  42788  kelac1  43039  imasgim  43076  lnrfg  43095  nvocnvb  43403  brco2f1o  44013  brco3f1o  44014  clsneikex  44087  clsneinex  44088  clsneiel1  44089  neicvgmex  44098  neicvgel1  44100  dssmapntrcls  44109  stoweidlem27  45966  stoweidlem31  45970  stoweidlem39  45978  fourierdlem20  46066  fourierdlem50  46095  fourierdlem52  46097  fourierdlem54  46099  fourierdlem64  46109  fourierdlem76  46121  fourierdlem102  46147  fourierdlem114  46159  sge0f1o  46321  nnfoctbdjlem  46394  isomenndlem  46469  ovnsubaddlem1  46509  3f1oss1  47008  reuf1odnf  47040  reuf1od  47041  f1oresf1o2  47224  fundcmpsurbijinjpreimafv  47315  fundcmpsurinjimaid  47319  grimfn  47783  isgrim  47786  isuspgrim0lem  47789  isuspgrim0  47790  uspgrimprop  47791  isuspgrim  47793  grimuhgr  47796  grimco  47798  gricushgr  47804  isubgrgrim  47815  uhgrimisgrgriclem  47816  uhgrimisgrgric  47817  clnbgrgrim  47820  grimedg  47821  grtriclwlk3  47830  grlimfn  47837  isgrlim  47840  uspgrlimlem1  47846  uspgrlimlem2  47847  uspgrlimlem3  47848  uspgrlimlem4  47849  grlimgrtrilem2  47853  grlictr  47866  1hegrlfgr  47926  funcringcsetcALTV2lem8  48091  funcringcsetclem8ALTV  48114  itcovalendof  48473  thincciso  48790  amgmwlem  48968