Theorem f1of 6708

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

Syntax hints:   → wi 4  ⟶wf 6422  –1-1→wf1 6423  –1-1-onto→wf1o 6425

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 206  df-an 397  df-f1 6431  df-f1o 6433

This theorem is referenced by:  f1ofn  6709  f1ompt  6977  f1oresrab  6991  fsn  6999  fsnunf  7049  f1ocnvfv1  7140  f1ocnvfv2  7141  fsnex  7147  f1ocnvdm  7149  fcof1oinvd  7157  fveqf1o  7167  isocnv  7193  isocnv3  7195  isores2  7196  isotr  7199  isofr2  7207  isopolem  7208  isosolem  7210  f1oiso2  7215  weniso  7217  f1ofveu  7262  f1oexrnex  7764  f1oabexg  7773  wemoiso  7805  suppsnop  7981  smoiso  8180  mapsnd  8661  ralxpmap  8671  f1oen2g  8743  en1  8798  en1OLD  8799  enfixsn  8855  mapen  8915  ac6sfi  9045  domunfican  9074  fiint  9078  mapfienlem1  9151  mapfienlem2  9152  mapfienlem3  9153  mapfien  9154  supisoex  9220  supiso  9221  ordiso2  9261  unxpwdom2  9334  cantnfle  9416  cantnfp1lem3  9425  cantnflem1b  9431  cantnflem1d  9433  cantnflem1  9434  cnfcomlem  9444  cnfcom  9445  cnfcom2lem  9446  cnfcom2  9447  cnfcom3lem  9448  cnfcom3  9449  cnfcom3clem  9450  djuin  9686  infxpenlem  9779  infxpenc  9784  infxpenc2lem2  9786  fseqenlem1  9790  acndom  9817  acndom2  9820  infpwfien  9828  iunfictbso  9880  infmap2  9984  ackbij2lem2  10006  infpssrlem3  10071  infpssrlem4  10072  fin23lem30  10108  isf32lem6  10124  isf32lem7  10125  isf32lem8  10126  enfin1ai  10150  axcc3  10204  axcclem  10223  ttukeylem7  10281  fpwwe2lem5  10401  fpwwe2lem6  10402  fpwwe2lem8  10404  canthp1lem2  10419  canthp1  10420  pwfseqlem4a  10427  pwfseqlem5  10429  axdc4uzlem  13713  seqf1olem1  13772  seqf1olem2  13773  seqf1o  13774  hashkf  14056  hasheqf1oi  14076  hasheqf1od  14078  hashcl  14081  hashgadd  14102  hashfacen  14176  hashfacenOLD  14177  hashf1lem1  14178  hashf1lem1OLD  14179  fz1isolem  14185  seqcoll  14188  seqcoll2  14189  cnrecnv  14886  sumeq2ii  15415  summolem3  15436  summolem2a  15437  fsum  15442  fsumf1o  15445  fsumss  15447  fsumcl2lem  15453  fsumadd  15462  fsummulc2  15506  fsumrelem  15529  ackbijnn  15550  prodeq2ii  15633  prodmolem3  15653  prodmolem2a  15654  fprod  15661  fprodf1o  15666  fprodss  15668  fprodser  15669  fprodcl2lem  15670  fprodmul  15680  fproddiv  15681  fprodn0  15699  fproddvdsd  16054  sadcaddlem  16174  sadadd2lem  16176  sadadd3  16178  sadaddlem  16183  sadasslem  16187  sadeq  16189  phimullem  16490  eulerthlem1  16492  eulerthlem2  16493  unbenlem  16619  vdwlem8  16699  0ram  16731  wunndx  16906  xpsaddlem  17294  xpsvsca  17298  xpsle  17300  idfucl  17606  setccatid  17809  setcinv  17815  catcisolem  17835  estrccatid  17858  funcestrcsetclem7  17873  funcestrcsetclem8  17874  funcsetcestrclem7  17888  funcsetcestrclem8  17889  yonffthlem  18010  gsumpropd2lem  18373  idmhm  18449  mhmf1o  18450  gsumws1  18486  ielefmnd  18536  idghm  18859  ghmf1o  18874  permsetexOLD  18987  symgbas  18988  elsymgbas  18991  symgbasf  18993  symgbasfi  18996  symg1bas  19008  symggrp  19018  lactghmga  19023  symgfixf1  19055  f1omvdmvd  19061  f1omvdconj  19064  f1omvdco2  19066  pmtrfconj  19084  symggen  19088  pmtrdifellem1  19094  pmtrdifellem2  19095  psgnunilem1  19111  gsumval3eu  19515  gsumval3lem1  19516  gsumval3  19518  gsumzf1o  19523  gsumconst  19545  gsumsub  19559  gsumcom2  19586  dprdfsub  19634  dprdf1o  19645  dprdsn  19649  ablfaclem2  19699  srngcl  20125  lmhmf1o  20318  fidomndrnglem  20588  gsumfsum  20675  zntoslem  20774  islinds2  21030  lindsmm  21045  psrass1lemOLD  21153  psrass1lem  21156  psrnegcl  21175  psrlinv  21176  coe1f2  21390  coe1add  21445  evls1rhmlem  21497  evl1sca  21510  pf1ind  21531  mat1dimelbas  21630  mat1f  21641  mdetleib2  21747  mdetrsca  21762  mdetralt  21767  mdetunilem7  21777  mdetunilem9  21779  ssidcn  22416  hmphdis  22957  indishmph  22959  cmphaushmeo  22961  ordthmeolem  22962  txhmeo  22964  qtopf1  22977  ufldom  23123  symgtgp  23267  tsmsf1o  23306  iducn  23445  imasdsf1olem  23536  xpsdsval  23544  imasf1obl  23654  icchmeo  24114  iccpnfcnv  24117  xrhmeo  24119  cnheiborlem  24127  ovolctb  24664  ovoliunlem1  24676  ovoliunlem2  24677  iunmbl2  24731  dyadmbl  24774  vitalilem2  24783  vitalilem3  24784  vitalilem4  24785  vitalilem5  24786  mbfid  24809  dvid  25092  dvexp  25127  dvcnvlem  25150  dvcnv  25151  dvcnvrelem2  25192  dvcnvre  25193  efcvx  25618  reefgim  25619  efif1olem4  25711  eff1olem  25714  logrncl  25733  relogcl  25741  dvrelog  25802  relogcn  25803  logcn  25812  logf1o2  25815  dvlog  25816  dvlog2  25818  advlog  25819  advlogexp  25820  logtayl  25825  logccv  25828  dvcxp1  25903  loglesqrt  25921  asinrebnd  26061  dvatan  26095  efrlim  26129  amgmlem  26149  lgamcvg2  26214  wilthlem2  26228  wilthlem3  26229  sqff1o  26341  lgsqrlem4  26507  logdivsum  26691  log2sumbnd  26702  isismt  26905  motcl  26910  motco  26911  cnvmot  26912  motgrp  26914  motcgrg  26915  f1otrg  27242  f1otrge  27243  axlowdimlem10  27329  axcontlem5  27346  axcontlem10  27351  upgrres1  27690  umgrres1  27691  upgriseupth  28579  pliguhgr  28856  dmadjrn  30265  unopnorm  30287  unopadj  30289  unoplin  30290  counop  30291  idcnop  30351  idhmop  30352  unopbd  30385  bracnln  30479  cnvbraval  30480  leopnmid  30508  nmopleid  30509  hmopidmch  30523  hmopidmpj  30524  disjrdx  30938  fmptco1f1o  30976  isoun  31042  padct  31062  fcobij  31065  fcobijfs  31066  abliso  31313  symgfcoeu  31359  symgcom  31360  pmtrcnel  31366  pmtrcnel2  31367  pmtrcnelor  31368  cycpmco2f1  31399  cycpmco2rn  31400  cycpmco2lem2  31402  cycpmco2lem3  31403  cycpmco2lem4  31404  cycpmco2lem5  31405  cycpmco2lem6  31406  cycpmco2lem7  31407  cycpmco2  31408  cycpmconjv  31417  cycpmconjslem1  31429  cycpmconjslem2  31430  cycpmconjs  31431  islinds5  31571  ellspds  31572  tpr2rico  31870  xrge0iifmhm  31897  xrge0pluscn  31898  rrhre  31979  esumf1o  32026  volmeas  32207  eulerpartgbij  32347  eulerpartlemmf  32350  eulerpartlemgvv  32351  eulerpartlemgf  32354  eulerpartlemgs2  32355  eulerpartlemn  32356  ballotlemsima  32490  reprpmtf1o  32614  logdivsqrle  32638  hgt750lemg  32642  deranglem  33136  derangsn  33140  derangenlem  33141  subfacp1lem4  33153  subfacp1lem5  33154  subfacp1lem6  33155  cvmfolem  33249  cvmliftlem6  33260  poimirlem1  35786  poimirlem2  35787  poimirlem3  35788  poimirlem4  35789  poimirlem6  35791  poimirlem7  35792  poimirlem9  35794  poimirlem11  35796  poimirlem12  35797  poimirlem16  35801  poimirlem17  35802  poimirlem19  35804  poimirlem20  35805  poimirlem22  35807  poimirlem26  35811  poimirlem27  35812  poimirlem28  35813  poimirlem32  35817  mblfinlem2  35823  dvasin  35869  f1ocan1fv  35892  metf1o  35921  ismtyval  35966  isismty  35967  ismtyima  35969  ismtyhmeolem  35970  ismtybndlem  35972  ismrer1  36004  reheibor  36005  grposnOLD  36048  rngoisocnv  36147  lflnegl  37098  lautset  38104  islaut  38105  lautcl  38109  lautco  38119  pautsetN  38120  ispautN  38121  ldilco  38138  ltrncoidN  38150  ltrncoval  38167  trlcoabs2N  38744  trlcoat  38745  trlcone  38750  cdlemg47a  38756  cdlemg46  38757  cdlemg47  38758  trljco  38762  tgrpgrplem  38771  tendoidcl  38791  tendo0co2  38810  tendo0pl  38813  cdlemi2  38841  cdlemk2  38854  cdlemk4  38856  cdlemk8  38860  cdlemkid2  38946  cdlemk45  38969  cdlemk53b  38978  cdlemk53  38979  cdlemk55a  38981  erng1r  39017  tendocnv  39043  dvalveclem  39047  dva0g  39049  dvhgrp  39129  dvh0g  39133  dvhopN  39138  cdlemn3  39219  cdlemn8  39226  cdlemn9  39227  dihordlem7b  39237  dihopelvalcpre  39270  dihmeetlem1N  39312  dihglblem5apreN  39313  lcfrlem13  39577  hvmapclN  39786  hvmapcl2  39788  dvrelog2  40080  dvrelog3  40081  sticksstones3  40112  sticksstones17  40127  sticksstones18  40128  sticksstones19  40129  metakunt33  40165  mapfzcons  40546  mzpresrename  40580  diophrw  40589  eldioph2  40592  diophren  40643  kelac1  40896  imasgim  40933  lnrfg  40952  brco2f1o  41623  brco3f1o  41624  clsneikex  41697  clsneinex  41698  clsneiel1  41699  neicvgmex  41708  neicvgel1  41710  dssmapntrcls  41719  stoweidlem27  43549  stoweidlem31  43553  stoweidlem39  43561  fourierdlem20  43649  fourierdlem50  43678  fourierdlem52  43680  fourierdlem54  43682  fourierdlem64  43692  fourierdlem76  43704  fourierdlem102  43730  fourierdlem114  43742  sge0f1o  43901  nnfoctbdjlem  43974  isomenndlem  44049  ovnsubaddlem1  44089  reuf1odnf  44577  reuf1od  44578  f1oresf1o2  44761  fundcmpsurbijinjpreimafv  44837  fundcmpsurinjimaid  44841  isomushgr  45256  isomuspgr  45264  isomgrtrlem  45268  1hegrlfgr  45272  mgmhmf1o  45319  idmgmhm  45320  funcringcsetcALTV2lem8  45579  funcringcsetclem8ALTV  45602  itcovalendof  45993  thincciso  46308  amgmwlem  46484