Theorem f1of 6774

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

Syntax hints:   → wi 4  ⟶wf 6488  –1-1→wf1 6489  –1-1-onto→wf1o 6491

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 6497  df-f1o 6499

This theorem is referenced by:  f1ofn  6775  f1ompt  7057  f1oresrab  7074  fsn  7082  fsnunf  7133  f1ounsn  7220  f1ocnvfv1  7224  f1ocnvfv2  7225  fsnex  7231  f1ocnvdm  7233  fcof1oinvd  7241  fveqf1o  7250  isocnv  7278  isocnv3  7280  isores2  7281  isotr  7284  isofr2  7292  isopolem  7293  isosolem  7295  f1oiso2  7300  weniso  7302  f1ofveu  7354  f1oexrnex  7871  f1oabexg  7886  f1oabexgOLD  7887  wemoiso  7919  mptcnfimad  7932  suppsnop  8121  smoiso  8295  mapsnd  8827  ralxpmap  8837  f1oen2g  8908  en1  8964  enfixsn  9017  mapen  9072  ac6sfi  9187  domunfican  9225  fiint  9230  mapfienlem1  9311  mapfienlem2  9312  mapfienlem3  9313  mapfien  9314  supisoex  9381  supiso  9382  ordiso2  9423  unxpwdom2  9496  cantnfle  9583  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1d  9600  cantnflem1  9601  cnfcomlem  9611  cnfcom  9612  cnfcom2lem  9613  cnfcom2  9614  cnfcom3lem  9615  cnfcom3  9616  cnfcom3clem  9617  djuin  9833  infxpenlem  9926  infxpenc  9931  infxpenc2lem2  9933  fseqenlem1  9937  acndom  9964  acndom2  9967  infpwfien  9975  iunfictbso  10027  infmap2  10130  ackbij2lem2  10152  infpssrlem3  10218  infpssrlem4  10219  fin23lem30  10255  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  enfin1ai  10297  axcc3  10351  axcclem  10370  ttukeylem7  10428  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  canthp1lem2  10567  canthp1  10568  pwfseqlem4a  10575  pwfseqlem5  10577  axdc4uzlem  13936  seqf1olem1  13994  seqf1olem2  13995  seqf1o  13996  hashkf  14285  hasheqf1oi  14304  hasheqf1od  14306  hashcl  14309  hashgadd  14330  hashfacen  14407  hashf1lem1  14408  fz1isolem  14414  seqcoll  14417  seqcoll2  14418  cnrecnv  15118  sumeq2ii  15646  summolem3  15667  summolem2a  15668  fsum  15673  fsumf1o  15676  fsumss  15678  fsumcl2lem  15684  fsumadd  15693  fsummulc2  15737  fsumrelem  15761  ackbijnn  15784  prodeq2ii  15867  prodmolem3  15889  prodmolem2a  15890  fprod  15897  fprodf1o  15902  fprodss  15904  fprodser  15905  fprodcl2lem  15906  fprodmul  15916  fproddiv  15917  fprodn0  15935  fproddvdsd  16295  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  unbenlem  16870  vdwlem8  16950  0ram  16982  wunndx  17156  xpsaddlem  17528  xpsvsca  17532  xpsle  17534  idfucl  17839  setccatid  18042  setcinv  18048  catcisolem  18068  estrccatid  18089  funcestrcsetclem7  18103  funcestrcsetclem8  18104  funcsetcestrclem7  18118  funcsetcestrclem8  18119  yonffthlem  18239  gsumpropd2lem  18638  mgmhmf1o  18659  idmgmhm  18660  idmhm  18754  mhmf1o  18755  gsumws1  18797  ielefmnd  18846  idghm  19197  ghmf1o  19214  symgbas  19338  elsymgbas  19340  symgbasf  19342  symgbasfi  19345  symg1bas  19357  symggrp  19366  lactghmga  19371  symgfixf1  19403  f1omvdmvd  19409  f1omvdconj  19412  f1omvdco2  19414  pmtrfconj  19432  symggen  19436  pmtrdifellem1  19442  pmtrdifellem2  19443  psgnunilem1  19459  gsumval3eu  19870  gsumval3lem1  19871  gsumval3  19873  gsumzf1o  19878  gsumconst  19900  gsumsub  19914  gsumcom2  19941  dprdfsub  19989  dprdf1o  20000  dprdsn  20004  ablfaclem2  20054  rngisomfv1  20436  rngisom1  20437  rngisomring1  20439  fidomndrnglem  20740  srngcl  20817  lmhmf1o  21033  gsumfsum  21424  zntoslem  21546  islinds2  21803  lindsmm  21818  psrass1lem  21922  psrnegcl  21943  psrlinv  21944  coe1f2  22183  coe1add  22239  evls1rhmlem  22296  evl1sca  22309  pf1ind  22330  mat1dimelbas  22446  mat1f  22457  mdetleib2  22563  mdetrsca  22578  mdetralt  22583  mdetunilem7  22593  mdetunilem9  22595  ssidcn  23230  hmphdis  23771  indishmph  23773  cmphaushmeo  23775  ordthmeolem  23776  txhmeo  23778  qtopf1  23791  ufldom  23937  symgtgp  24081  tsmsf1o  24120  iducn  24257  imasdsf1olem  24348  xpsdsval  24356  imasf1obl  24463  icchmeo  24918  iccpnfcnv  24921  xrhmeo  24923  cnheiborlem  24931  ovolctb  25467  ovoliunlem1  25479  ovoliunlem2  25480  iunmbl2  25534  dyadmbl  25577  vitalilem2  25586  vitalilem3  25587  vitalilem4  25588  vitalilem5  25589  mbfid  25612  dvid  25895  dvexp  25930  dvcnvlem  25953  dvcnv  25954  dvcnvrelem2  25995  dvcnvre  25996  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  26738  asinrebnd  26878  dvatan  26912  efrlim  26946  efrlimOLD  26947  amgmlem  26967  lgamcvg2  27032  wilthlem2  27046  wilthlem3  27047  sqff1o  27159  lgsqrlem4  27326  logdivsum  27510  log2sumbnd  27521  isismt  28616  motcl  28621  motco  28622  cnvmot  28623  motgrp  28625  motcgrg  28626  f1otrg  28953  f1otrge  28954  axlowdimlem10  29034  axcontlem5  29051  axcontlem10  29056  uspgriedgedg  29259  upgrres1  29396  umgrres1  29397  upgriseupth  30292  pliguhgr  30572  dmadjrn  31981  unopnorm  32003  unopadj  32005  unoplin  32006  counop  32007  idcnop  32067  idhmop  32068  unopbd  32101  bracnln  32195  cnvbraval  32196  leopnmid  32224  nmopleid  32225  hmopidmch  32239  hmopidmpj  32240  disjrdx  32676  fmptco1f1o  32721  isoun  32790  padct  32806  fcobij  32808  fcobijfs  32809  fcobijfs2  32810  wrdpmcl  33013  ccatws1f1o  33026  ccatws1f1olast  33027  mndlactf1o  33105  mndractf1o  33106  abliso  33111  symgfcoeu  33158  symgcom  33159  pmtrcnel  33165  pmtrcnel2  33166  pmtrcnelor  33167  wrdpmtrlast  33169  cycpmco2f1  33200  cycpmco2rn  33201  cycpmco2lem2  33203  cycpmco2lem3  33204  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmco2  33209  cycpmconjv  33218  cycpmconjslem1  33230  cycpmconjslem2  33231  cycpmconjs  33232  islinds5  33442  ellspds  33443  1arithidomlem1  33610  1arithidomlem2  33611  1arithidom  33612  mplvrpmlem  33702  mplvrpmfgalem  33703  mplvrpmmhm  33705  mplvrpmrhm  33706  esplyfval0  33723  esplylem  33725  esplympl  33726  esplymhp  33727  esplyfv1  33728  esplyfv  33729  esplysply  33730  esplyfval3  33731  vieta  33739  tpr2rico  34072  xrge0iifmhm  34099  xrge0pluscn  34100  rrhre  34181  esumf1o  34210  volmeas  34391  eulerpartgbij  34532  eulerpartlemmf  34535  eulerpartlemgvv  34536  eulerpartlemgf  34539  eulerpartlemgs2  34540  eulerpartlemn  34541  ballotlemsima  34676  reprpmtf1o  34786  logdivsqrle  34810  hgt750lemg  34814  vonf1owev  35306  deranglem  35364  derangsn  35368  derangenlem  35369  subfacp1lem4  35381  subfacp1lem5  35382  subfacp1lem6  35383  cvmfolem  35477  cvmliftlem6  35488  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem32  37987  mblfinlem2  37993  dvasin  38039  f1ocan1fv  38061  metf1o  38090  ismtyval  38135  isismty  38136  ismtyima  38138  ismtyhmeolem  38139  ismtybndlem  38141  ismrer1  38173  reheibor  38174  grposnOLD  38217  rngoisocnv  38316  lflnegl  39536  lautset  40542  islaut  40543  lautcl  40547  lautco  40557  pautsetN  40558  ispautN  40559  ldilco  40576  ltrncoidN  40588  ltrncoval  40605  trlcoabs2N  41182  trlcoat  41183  trlcone  41188  cdlemg47a  41194  cdlemg46  41195  cdlemg47  41196  trljco  41200  tgrpgrplem  41209  tendoidcl  41229  tendo0co2  41248  tendo0pl  41251  cdlemi2  41279  cdlemk2  41292  cdlemk4  41294  cdlemk8  41298  cdlemkid2  41384  cdlemk45  41407  cdlemk53b  41416  cdlemk53  41417  cdlemk55a  41419  erng1r  41455  tendocnv  41481  dvalveclem  41485  dva0g  41487  dvhgrp  41567  dvh0g  41571  dvhopN  41576  cdlemn3  41657  cdlemn8  41664  cdlemn9  41665  dihordlem7b  41675  dihopelvalcpre  41708  dihmeetlem1N  41750  dihglblem5apreN  41751  lcfrlem13  42015  hvmapclN  42224  hvmapcl2  42226  dvrelog2  42517  dvrelog3  42518  sticksstones3  42601  sticksstones17  42616  sticksstones18  42617  sticksstones19  42618  readvrec2  42807  readvrec  42808  mapfzcons  43162  mzpresrename  43196  diophrw  43205  eldioph2  43208  diophren  43259  kelac1  43509  imasgim  43546  lnrfg  43565  nvocnvb  43867  brco2f1o  44477  brco3f1o  44478  clsneikex  44551  clsneinex  44552  clsneiel1  44553  neicvgmex  44562  neicvgel1  44564  dssmapntrcls  44573  stoweidlem27  46473  stoweidlem31  46477  stoweidlem39  46485  fourierdlem20  46573  fourierdlem50  46602  fourierdlem52  46604  fourierdlem54  46606  fourierdlem64  46616  fourierdlem76  46628  fourierdlem102  46654  fourierdlem114  46666  sge0f1o  46828  nnfoctbdjlem  46901  isomenndlem  46976  ovnsubaddlem1  47016  3f1oss1  47535  reuf1odnf  47567  reuf1od  47568  f1oresf1o2  47751  fundcmpsurbijinjpreimafv  47879  fundcmpsurinjimaid  47883  grimfn  48367  isgrim  48370  grimuhgr  48375  grimco  48377  uhgrimedgi  48378  isuspgrim0lem  48381  isuspgrim0  48382  isuspgrim  48384  upgrimwlklem4  48388  gricushgr  48405  isubgrgrim  48417  uhgrimisgrgriclem  48418  uhgrimisgrgric  48419  clnbgrgrim  48422  grimedg  48423  grtriclwlk3  48433  isubgr3stgrlem3  48456  isubgr3stgrlem4  48457  isubgr3stgrlem6  48459  isubgr3stgrlem7  48460  isubgr3stgrlem8  48461  isubgr3stgrlem9  48462  grlimfn  48467  isgrlim  48470  uspgrlimlem1  48476  uspgrlimlem2  48477  uspgrlimlem3  48478  uspgrlimlem4  48479  grlimprclnbgredg  48485  grlimgredgex  48488  grlimgrtrilem2  48490  grlictr  48503  clnbgr3stgrgrlim  48507  clnbgr3stgrgrlic  48508  1hegrlfgr  48620  funcringcsetcALTV2lem8  48785  funcringcsetclem8ALTV  48808  itcovalendof  49157  uptrlem1  49697  uptr2  49708  swapf2f1oaALT  49765  swapfcoa  49768  swapffunc  49769  fucoppc  49897  thincciso  49940  thinccisod  49941  lmdran  50158  cmdlan  50159  amgmwlem  50289