Theorem f1of 6800

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

Syntax hints:   → wi 4  ⟶wf 6507  –1-1→wf1 6508  –1-1-onto→wf1o 6510

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 6516  df-f1o 6518

This theorem is referenced by:  f1ofn  6801  f1ompt  7083  f1oresrab  7099  fsn  7107  fsnunf  7159  f1ounsn  7247  f1ocnvfv1  7251  f1ocnvfv2  7252  fsnex  7258  f1ocnvdm  7260  fcof1oinvd  7268  fveqf1o  7277  isocnv  7305  isocnv3  7307  isores2  7308  isotr  7311  isofr2  7319  isopolem  7320  isosolem  7322  f1oiso2  7327  weniso  7329  f1ofveu  7381  f1oexrnex  7903  f1oabexg  7918  f1oabexgOLD  7919  wemoiso  7952  mptcnfimad  7965  suppsnop  8157  smoiso  8331  mapsnd  8859  ralxpmap  8869  f1oen2g  8940  en1  8995  enfixsn  9050  mapen  9105  ac6sfi  9231  domunfican  9272  fiint  9277  fiintOLD  9278  mapfienlem1  9356  mapfienlem2  9357  mapfienlem3  9358  mapfien  9359  supisoex  9426  supiso  9427  ordiso2  9468  unxpwdom2  9541  cantnfle  9624  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1d  9641  cantnflem1  9642  cnfcomlem  9652  cnfcom  9653  cnfcom2lem  9654  cnfcom2  9655  cnfcom3lem  9656  cnfcom3  9657  cnfcom3clem  9658  djuin  9871  infxpenlem  9966  infxpenc  9971  infxpenc2lem2  9973  fseqenlem1  9977  acndom  10004  acndom2  10007  infpwfien  10015  iunfictbso  10067  infmap2  10170  ackbij2lem2  10192  infpssrlem3  10258  infpssrlem4  10259  fin23lem30  10295  isf32lem6  10311  isf32lem7  10312  isf32lem8  10313  enfin1ai  10337  axcc3  10391  axcclem  10410  ttukeylem7  10468  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  canthp1lem2  10606  canthp1  10607  pwfseqlem4a  10614  pwfseqlem5  10616  axdc4uzlem  13948  seqf1olem1  14006  seqf1olem2  14007  seqf1o  14008  hashkf  14297  hasheqf1oi  14316  hasheqf1od  14318  hashcl  14321  hashgadd  14342  hashfacen  14419  hashf1lem1  14420  fz1isolem  14426  seqcoll  14429  seqcoll2  14430  cnrecnv  15131  sumeq2ii  15659  summolem3  15680  summolem2a  15681  fsum  15686  fsumf1o  15689  fsumss  15691  fsumcl2lem  15697  fsumadd  15706  fsummulc2  15750  fsumrelem  15773  ackbijnn  15794  prodeq2ii  15877  prodmolem3  15899  prodmolem2a  15900  fprod  15907  fprodf1o  15912  fprodss  15914  fprodser  15915  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodn0  15945  fproddvdsd  16305  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  sadeq  16442  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  unbenlem  16879  vdwlem8  16959  0ram  16991  wunndx  17165  xpsaddlem  17536  xpsvsca  17540  xpsle  17542  idfucl  17843  setccatid  18046  setcinv  18052  catcisolem  18072  estrccatid  18093  funcestrcsetclem7  18107  funcestrcsetclem8  18108  funcsetcestrclem7  18122  funcsetcestrclem8  18123  yonffthlem  18243  gsumpropd2lem  18606  mgmhmf1o  18627  idmgmhm  18628  idmhm  18722  mhmf1o  18723  gsumws1  18765  ielefmnd  18814  idghm  19163  ghmf1o  19180  symgbas  19302  elsymgbas  19304  symgbasf  19306  symgbasfi  19309  symg1bas  19321  symggrp  19330  lactghmga  19335  symgfixf1  19367  f1omvdmvd  19373  f1omvdconj  19376  f1omvdco2  19378  pmtrfconj  19396  symggen  19400  pmtrdifellem1  19406  pmtrdifellem2  19407  psgnunilem1  19423  gsumval3eu  19834  gsumval3lem1  19835  gsumval3  19837  gsumzf1o  19842  gsumconst  19864  gsumsub  19878  gsumcom2  19905  dprdfsub  19953  dprdf1o  19964  dprdsn  19968  ablfaclem2  20018  rngisomfv1  20374  rngisom1  20375  rngisomring1  20377  fidomndrnglem  20681  srngcl  20758  lmhmf1o  20953  gsumfsum  21351  zntoslem  21466  islinds2  21722  lindsmm  21737  psrass1lem  21841  psrnegcl  21863  psrlinv  21864  coe1f2  22094  coe1add  22150  evls1rhmlem  22208  evl1sca  22221  pf1ind  22242  mat1dimelbas  22358  mat1f  22369  mdetleib2  22475  mdetrsca  22490  mdetralt  22495  mdetunilem7  22505  mdetunilem9  22507  ssidcn  23142  hmphdis  23683  indishmph  23685  cmphaushmeo  23687  ordthmeolem  23688  txhmeo  23690  qtopf1  23703  ufldom  23849  symgtgp  23993  tsmsf1o  24032  iducn  24170  imasdsf1olem  24261  xpsdsval  24269  imasf1obl  24376  icchmeo  24838  icchmeoOLD  24839  iccpnfcnv  24842  xrhmeo  24844  cnheiborlem  24853  ovolctb  25391  ovoliunlem1  25403  ovoliunlem2  25404  iunmbl2  25458  dyadmbl  25501  vitalilem2  25510  vitalilem3  25511  vitalilem4  25512  vitalilem5  25513  mbfid  25536  dvid  25819  dvexp  25857  dvcnvlem  25880  dvcnv  25881  dvcnvrelem2  25923  dvcnvre  25924  efcvx  26359  reefgim  26360  efif1olem4  26454  eff1olem  26457  logrncl  26476  relogcl  26484  dvrelog  26546  relogcn  26547  logcn  26556  logf1o2  26559  dvlog  26560  dvlog2  26562  advlog  26563  advlogexp  26564  logtayl  26569  logccv  26572  dvcxp1  26649  loglesqrt  26671  asinrebnd  26811  dvatan  26845  efrlim  26879  efrlimOLD  26880  amgmlem  26900  lgamcvg2  26965  wilthlem2  26979  wilthlem3  26980  sqff1o  27092  lgsqrlem4  27260  logdivsum  27444  log2sumbnd  27455  isismt  28461  motcl  28466  motco  28467  cnvmot  28468  motgrp  28470  motcgrg  28471  f1otrg  28798  f1otrge  28799  axlowdimlem10  28878  axcontlem5  28895  axcontlem10  28900  uspgriedgedg  29103  upgrres1  29240  umgrres1  29241  upgriseupth  30136  pliguhgr  30415  dmadjrn  31824  unopnorm  31846  unopadj  31848  unoplin  31849  counop  31850  idcnop  31910  idhmop  31911  unopbd  31944  bracnln  32038  cnvbraval  32039  leopnmid  32067  nmopleid  32068  hmopidmch  32082  hmopidmpj  32083  disjrdx  32520  fmptco1f1o  32557  isoun  32625  padct  32643  fcobij  32645  fcobijfs  32646  wrdpmcl  32859  ccatws1f1o  32873  ccatws1f1olast  32874  mndlactf1o  32971  mndractf1o  32972  abliso  32977  symgfcoeu  33039  symgcom  33040  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  wrdpmtrlast  33050  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  cycpmconjv  33099  cycpmconjslem1  33111  cycpmconjslem2  33112  cycpmconjs  33113  islinds5  33338  ellspds  33339  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  tpr2rico  33902  xrge0iifmhm  33929  xrge0pluscn  33930  rrhre  34011  esumf1o  34040  volmeas  34221  eulerpartgbij  34363  eulerpartlemmf  34366  eulerpartlemgvv  34367  eulerpartlemgf  34370  eulerpartlemgs2  34371  eulerpartlemn  34372  ballotlemsima  34507  reprpmtf1o  34617  logdivsqrle  34641  hgt750lemg  34645  vonf1owev  35095  deranglem  35153  derangsn  35157  derangenlem  35158  subfacp1lem4  35170  subfacp1lem5  35171  subfacp1lem6  35172  cvmfolem  35266  cvmliftlem6  35277  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem32  37646  mblfinlem2  37652  dvasin  37698  f1ocan1fv  37720  metf1o  37749  ismtyval  37794  isismty  37795  ismtyima  37797  ismtyhmeolem  37798  ismtybndlem  37800  ismrer1  37832  reheibor  37833  grposnOLD  37876  rngoisocnv  37975  lflnegl  39069  lautset  40076  islaut  40077  lautcl  40081  lautco  40091  pautsetN  40092  ispautN  40093  ldilco  40110  ltrncoidN  40122  ltrncoval  40139  trlcoabs2N  40716  trlcoat  40717  trlcone  40722  cdlemg47a  40728  cdlemg46  40729  cdlemg47  40730  trljco  40734  tgrpgrplem  40743  tendoidcl  40763  tendo0co2  40782  tendo0pl  40785  cdlemi2  40813  cdlemk2  40826  cdlemk4  40828  cdlemk8  40832  cdlemkid2  40918  cdlemk45  40941  cdlemk53b  40950  cdlemk53  40951  cdlemk55a  40953  erng1r  40989  tendocnv  41015  dvalveclem  41019  dva0g  41021  dvhgrp  41101  dvh0g  41105  dvhopN  41110  cdlemn3  41191  cdlemn8  41198  cdlemn9  41199  dihordlem7b  41209  dihopelvalcpre  41242  dihmeetlem1N  41284  dihglblem5apreN  41285  lcfrlem13  41549  hvmapclN  41758  hvmapcl2  41760  dvrelog2  42052  dvrelog3  42053  sticksstones3  42136  sticksstones17  42151  sticksstones18  42152  sticksstones19  42153  readvrec2  42349  readvrec  42350  mapfzcons  42704  mzpresrename  42738  diophrw  42747  eldioph2  42750  diophren  42801  kelac1  43052  imasgim  43089  lnrfg  43108  nvocnvb  43411  brco2f1o  44021  brco3f1o  44022  clsneikex  44095  clsneinex  44096  clsneiel1  44097  neicvgmex  44106  neicvgel1  44108  dssmapntrcls  44117  stoweidlem27  46025  stoweidlem31  46029  stoweidlem39  46037  fourierdlem20  46125  fourierdlem50  46154  fourierdlem52  46156  fourierdlem54  46158  fourierdlem64  46168  fourierdlem76  46180  fourierdlem102  46206  fourierdlem114  46218  sge0f1o  46380  nnfoctbdjlem  46453  isomenndlem  46528  ovnsubaddlem1  46568  3f1oss1  47076  reuf1odnf  47108  reuf1od  47109  f1oresf1o2  47292  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  grimfn  47879  isgrim  47882  grimuhgr  47887  grimco  47889  uhgrimedgi  47890  isuspgrim0lem  47893  isuspgrim0  47894  isuspgrim  47896  upgrimwlklem4  47900  gricushgr  47917  isubgrgrim  47929  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrim  47934  grimedg  47935  grtriclwlk3  47944  isubgr3stgrlem3  47967  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  isubgr3stgrlem8  47972  isubgr3stgrlem9  47973  grlimfn  47978  isgrlim  47981  uspgrlimlem1  47987  uspgrlimlem2  47988  uspgrlimlem3  47989  uspgrlimlem4  47990  grlimgrtrilem2  47994  grlictr  48007  clnbgr3stgrgrlic  48011  1hegrlfgr  48120  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  itcovalendof  48658  uptrlem1  49199  uptr2  49210  swapf2f1oaALT  49267  swapfcoa  49270  swapffunc  49271  fucoppc  49399  thincciso  49442  thinccisod  49443  lmdran  49660  cmdlan  49661  amgmwlem  49791