Theorem f1of 6834

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

Syntax hints:   → wi 4  ⟶wf 6539  –1-1→wf1 6540  –1-1-onto→wf1o 6542

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 396  df-f1 6548  df-f1o 6550

This theorem is referenced by:  f1ofn  6835  f1ompt  7116  f1oresrab  7131  fsn  7139  fsnunf  7189  f1ocnvfv1  7280  f1ocnvfv2  7281  fsnex  7287  f1ocnvdm  7289  fcof1oinvd  7297  fveqf1o  7307  isocnv  7333  isocnv3  7335  isores2  7336  isotr  7339  isofr2  7347  isopolem  7348  isosolem  7350  f1oiso2  7355  weniso  7357  f1ofveu  7409  f1oexrnex  7930  f1oabexg  7939  wemoiso  7972  mptcnfimad  7985  suppsnop  8177  smoiso  8377  mapsnd  8899  ralxpmap  8909  f1oen2g  8983  en1  9040  en1OLD  9041  enfixsn  9100  mapen  9160  ac6sfi  9306  domunfican  9339  fiint  9343  mapfienlem1  9423  mapfienlem2  9424  mapfienlem3  9425  mapfien  9426  supisoex  9492  supiso  9493  ordiso2  9533  unxpwdom2  9606  cantnfle  9689  cantnfp1lem3  9698  cantnflem1b  9704  cantnflem1d  9706  cantnflem1  9707  cnfcomlem  9717  cnfcom  9718  cnfcom2lem  9719  cnfcom2  9720  cnfcom3lem  9721  cnfcom3  9722  cnfcom3clem  9723  djuin  9936  infxpenlem  10031  infxpenc  10036  infxpenc2lem2  10038  fseqenlem1  10042  acndom  10069  acndom2  10072  infpwfien  10080  iunfictbso  10132  infmap2  10236  ackbij2lem2  10258  infpssrlem3  10323  infpssrlem4  10324  fin23lem30  10360  isf32lem6  10376  isf32lem7  10377  isf32lem8  10378  enfin1ai  10402  axcc3  10456  axcclem  10475  ttukeylem7  10533  fpwwe2lem5  10653  fpwwe2lem6  10654  fpwwe2lem8  10656  canthp1lem2  10671  canthp1  10672  pwfseqlem4a  10679  pwfseqlem5  10681  axdc4uzlem  13975  seqf1olem1  14033  seqf1olem2  14034  seqf1o  14035  hashkf  14318  hasheqf1oi  14337  hasheqf1od  14339  hashcl  14342  hashgadd  14363  hashfacen  14440  hashfacenOLD  14441  hashf1lem1  14442  hashf1lem1OLD  14443  fz1isolem  14449  seqcoll  14452  seqcoll2  14453  cnrecnv  15139  sumeq2ii  15666  summolem3  15687  summolem2a  15688  fsum  15693  fsumf1o  15696  fsumss  15698  fsumcl2lem  15704  fsumadd  15713  fsummulc2  15757  fsumrelem  15780  ackbijnn  15801  prodeq2ii  15884  prodmolem3  15904  prodmolem2a  15905  fprod  15912  fprodf1o  15917  fprodss  15919  fprodser  15920  fprodcl2lem  15921  fprodmul  15931  fproddiv  15932  fprodn0  15950  fproddvdsd  16306  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  sadeq  16441  phimullem  16742  eulerthlem1  16744  eulerthlem2  16745  unbenlem  16871  vdwlem8  16951  0ram  16983  wunndx  17158  xpsaddlem  17549  xpsvsca  17553  xpsle  17555  idfucl  17861  setccatid  18067  setcinv  18073  catcisolem  18093  estrccatid  18116  funcestrcsetclem7  18131  funcestrcsetclem8  18132  funcsetcestrclem7  18146  funcsetcestrclem8  18147  yonffthlem  18268  gsumpropd2lem  18633  mgmhmf1o  18654  idmgmhm  18655  idmhm  18746  mhmf1o  18747  gsumws1  18784  ielefmnd  18833  idghm  19179  ghmf1o  19196  permsetexOLD  19318  symgbas  19319  elsymgbas  19322  symgbasf  19324  symgbasfi  19327  symg1bas  19339  symggrp  19349  lactghmga  19354  symgfixf1  19386  f1omvdmvd  19392  f1omvdconj  19395  f1omvdco2  19397  pmtrfconj  19415  symggen  19419  pmtrdifellem1  19425  pmtrdifellem2  19426  psgnunilem1  19442  gsumval3eu  19853  gsumval3lem1  19854  gsumval3  19856  gsumzf1o  19861  gsumconst  19883  gsumsub  19897  gsumcom2  19924  dprdfsub  19972  dprdf1o  19983  dprdsn  19987  ablfaclem2  20037  rngisomfv1  20398  rngisom1  20399  rngisomring1  20401  srngcl  20729  lmhmf1o  20925  fidomndrnglem  21254  gsumfsum  21361  zntoslem  21484  islinds2  21741  lindsmm  21756  psrass1lemOLD  21868  psrass1lem  21871  psrnegcl  21891  psrlinv  21892  coe1f2  22122  coe1add  22177  evls1rhmlem  22234  evl1sca  22247  pf1ind  22268  mat1dimelbas  22367  mat1f  22378  mdetleib2  22484  mdetrsca  22499  mdetralt  22504  mdetunilem7  22514  mdetunilem9  22516  ssidcn  23153  hmphdis  23694  indishmph  23696  cmphaushmeo  23698  ordthmeolem  23699  txhmeo  23701  qtopf1  23714  ufldom  23860  symgtgp  24004  tsmsf1o  24043  iducn  24182  imasdsf1olem  24273  xpsdsval  24281  imasf1obl  24391  icchmeo  24859  icchmeoOLD  24860  iccpnfcnv  24863  xrhmeo  24865  cnheiborlem  24874  ovolctb  25413  ovoliunlem1  25425  ovoliunlem2  25426  iunmbl2  25480  dyadmbl  25523  vitalilem2  25532  vitalilem3  25533  vitalilem4  25534  vitalilem5  25535  mbfid  25558  dvid  25841  dvexp  25879  dvcnvlem  25902  dvcnv  25903  dvcnvrelem2  25945  dvcnvre  25946  efcvx  26380  reefgim  26381  efif1olem4  26473  eff1olem  26476  logrncl  26495  relogcl  26503  dvrelog  26565  relogcn  26566  logcn  26575  logf1o2  26578  dvlog  26579  dvlog2  26581  advlog  26582  advlogexp  26583  logtayl  26588  logccv  26591  dvcxp1  26668  loglesqrt  26687  asinrebnd  26827  dvatan  26861  efrlim  26895  efrlimOLD  26896  amgmlem  26916  lgamcvg2  26981  wilthlem2  26995  wilthlem3  26996  sqff1o  27108  lgsqrlem4  27276  logdivsum  27460  log2sumbnd  27471  isismt  28332  motcl  28337  motco  28338  cnvmot  28339  motgrp  28341  motcgrg  28342  f1otrg  28669  f1otrge  28670  axlowdimlem10  28756  axcontlem5  28773  axcontlem10  28778  uspgriedgedg  28983  upgrres1  29120  umgrres1  29121  upgriseupth  30011  pliguhgr  30290  dmadjrn  31699  unopnorm  31721  unopadj  31723  unoplin  31724  counop  31725  idcnop  31785  idhmop  31786  unopbd  31819  bracnln  31913  cnvbraval  31914  leopnmid  31942  nmopleid  31943  hmopidmch  31957  hmopidmpj  31958  disjrdx  32375  fmptco1f1o  32412  isoun  32476  padct  32496  fcobij  32499  fcobijfs  32500  abliso  32751  symgfcoeu  32800  symgcom  32801  pmtrcnel  32807  pmtrcnel2  32808  pmtrcnelor  32809  cycpmco2f1  32840  cycpmco2rn  32841  cycpmco2lem2  32843  cycpmco2lem3  32844  cycpmco2lem4  32845  cycpmco2lem5  32846  cycpmco2lem6  32847  cycpmco2lem7  32848  cycpmco2  32849  cycpmconjv  32858  cycpmconjslem1  32870  cycpmconjslem2  32871  cycpmconjs  32872  islinds5  33074  ellspds  33075  tpr2rico  33508  xrge0iifmhm  33535  xrge0pluscn  33536  rrhre  33617  esumf1o  33664  volmeas  33845  eulerpartgbij  33987  eulerpartlemmf  33990  eulerpartlemgvv  33991  eulerpartlemgf  33994  eulerpartlemgs2  33995  eulerpartlemn  33996  ballotlemsima  34130  reprpmtf1o  34253  logdivsqrle  34277  hgt750lemg  34281  deranglem  34771  derangsn  34775  derangenlem  34776  subfacp1lem4  34788  subfacp1lem5  34789  subfacp1lem6  34790  cvmfolem  34884  cvmliftlem6  34895  poimirlem1  37089  poimirlem2  37090  poimirlem3  37091  poimirlem4  37092  poimirlem6  37094  poimirlem7  37095  poimirlem9  37097  poimirlem11  37099  poimirlem12  37100  poimirlem16  37104  poimirlem17  37105  poimirlem19  37107  poimirlem20  37108  poimirlem22  37110  poimirlem26  37114  poimirlem27  37115  poimirlem28  37116  poimirlem32  37120  mblfinlem2  37126  dvasin  37172  f1ocan1fv  37194  metf1o  37223  ismtyval  37268  isismty  37269  ismtyima  37271  ismtyhmeolem  37272  ismtybndlem  37274  ismrer1  37306  reheibor  37307  grposnOLD  37350  rngoisocnv  37449  lflnegl  38543  lautset  39550  islaut  39551  lautcl  39555  lautco  39565  pautsetN  39566  ispautN  39567  ldilco  39584  ltrncoidN  39596  ltrncoval  39613  trlcoabs2N  40190  trlcoat  40191  trlcone  40196  cdlemg47a  40202  cdlemg46  40203  cdlemg47  40204  trljco  40208  tgrpgrplem  40217  tendoidcl  40237  tendo0co2  40256  tendo0pl  40259  cdlemi2  40287  cdlemk2  40300  cdlemk4  40302  cdlemk8  40306  cdlemkid2  40392  cdlemk45  40415  cdlemk53b  40424  cdlemk53  40425  cdlemk55a  40427  erng1r  40463  tendocnv  40489  dvalveclem  40493  dva0g  40495  dvhgrp  40575  dvh0g  40579  dvhopN  40584  cdlemn3  40665  cdlemn8  40672  cdlemn9  40673  dihordlem7b  40683  dihopelvalcpre  40716  dihmeetlem1N  40758  dihglblem5apreN  40759  lcfrlem13  41023  hvmapclN  41232  hvmapcl2  41234  dvrelog2  41530  dvrelog3  41531  sticksstones3  41615  sticksstones17  41630  sticksstones18  41631  sticksstones19  41632  metakunt33  41680  mapfzcons  42127  mzpresrename  42161  diophrw  42170  eldioph2  42173  diophren  42224  kelac1  42478  imasgim  42515  lnrfg  42534  nvocnvb  42843  brco2f1o  43453  brco3f1o  43454  clsneikex  43527  clsneinex  43528  clsneiel1  43529  neicvgmex  43538  neicvgel1  43540  dssmapntrcls  43549  stoweidlem27  45406  stoweidlem31  45410  stoweidlem39  45418  fourierdlem20  45506  fourierdlem50  45535  fourierdlem52  45537  fourierdlem54  45539  fourierdlem64  45549  fourierdlem76  45561  fourierdlem102  45587  fourierdlem114  45599  sge0f1o  45761  nnfoctbdjlem  45834  isomenndlem  45909  ovnsubaddlem1  45949  reuf1odnf  46478  reuf1od  46479  f1oresf1o2  46662  fundcmpsurbijinjpreimafv  46738  fundcmpsurinjimaid  46742  grimfn  47154  isgrim  47157  isuspgrim0lem  47160  isuspgrim0  47161  uspgrimprop  47162  isuspgrim  47164  grimuhgr  47167  grimco  47169  gricushgr  47174  1hegrlfgr  47185  funcringcsetcALTV2lem8  47350  funcringcsetclem8ALTV  47373  itcovalendof  47733  thincciso  48046  amgmwlem  48226

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »