MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1of Structured version   Unicode version

Theorem f1of 5636
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 5635 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5601 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   -->wf 5409   -1-1->wf1 5410   -1-1-onto->wf1o 5412
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 185  df-an 371  df-f1 5418  df-f1o 5420
This theorem is referenced by:  f1ofn  5637  f1ompt  5860  f1oresrab  5870  fsn  5876  fsnunf  5911  f1ocnvfv1  5978  f1ocnvfv2  5979  f1ocnvdm  5984  fcof1o  5992  fveqf1o  5995  isocnv  6016  isocnv3  6018  isores2  6019  isotr  6022  isofr2  6030  isopolem  6031  isosolem  6033  f1oiso2  6038  weniso  6040  f1ofveu  6081  f1oexrnex  6522  f1oabexg  6531  wemoiso  6557  suppsnop  6699  smoiso  6815  mapsn  7246  ralxpmap  7254  f1oen2g  7318  en1  7368  enfixsn  7412  mapen  7467  ac6sfi  7548  domunfican  7576  fiint  7580  mapfienlem1  7646  mapfienlem2  7647  mapfienlem3  7648  mapfien  7649  supisoex  7713  supiso  7714  ordiso2  7721  ordtypelem10  7733  hartogslem1  7748  unxpwdom2  7795  cantnfle  7871  cantnfp1lem3  7880  cantnflem1b  7886  cantnflem1d  7888  cantnflem1  7889  cantnfleOLD  7901  cantnfp1lem3OLD  7906  cantnflem1bOLD  7909  cantnflem1dOLD  7911  cantnflem1OLD  7912  mapfienOLD  7919  cnfcomlem  7924  cnfcom  7925  cnfcom2lem  7926  cnfcom2  7927  cnfcom3lem  7928  cnfcom3  7929  cnfcom3clem  7930  cnfcomlemOLD  7932  cnfcomOLD  7933  cnfcom2lemOLD  7934  cnfcom2OLD  7935  cnfcom3lemOLD  7936  cnfcom3OLD  7937  cnfcom3clemOLD  7938  infxpenlem  8172  infxpenc  8176  infxpenc2lem2  8178  infxpencOLD  8181  infxpenc2lem2OLD  8182  fseqenlem1  8186  acndom  8213  acndom2  8216  infpwfien  8224  iunfictbso  8276  infmap2  8379  ackbij2lem2  8401  infpssrlem3  8466  infpssrlem4  8467  fin23lem30  8503  isf32lem6  8519  isf32lem7  8520  isf32lem8  8521  enfin1ai  8545  axcc3  8599  axcclem  8618  ttukeylem7  8676  fpwwe2lem6  8794  fpwwe2lem7  8795  fpwwe2lem9  8797  canthp1lem2  8812  canthp1  8813  pwfseqlem4a  8820  pwfseqlem5  8822  dfle2  11116  axdc4uzlem  11796  seqf1olem1  11837  seqf1olem2  11838  seqf1o  11839  hashkf  12097  hasheqf1oi  12114  hashcl  12118  hashgadd  12132  hashfacen  12199  hashf1lem1  12200  fz1isolem  12206  seqcoll  12208  seqcoll2  12209  snopiswrd  12235  cnrecnv  12646  sumeq2ii  13162  summolem3  13183  summolem2a  13184  fsum  13189  fsumf1o  13192  fsumss  13194  fsumcl2lem  13200  fsumadd  13207  fsummulc2  13243  fsumrelem  13262  ackbijnn  13283  sadcaddlem  13645  sadadd2lem  13647  sadadd3  13649  sadaddlem  13654  sadasslem  13658  sadeq  13660  phimullem  13846  eulerthlem1  13848  eulerthlem2  13849  unbenlem  13961  vdwlem8  14041  0ram  14073  wunndx  14182  xpsaddlem  14505  xpsvsca  14509  xpsle  14511  idfucl  14783  setccatid  14944  setcinv  14950  catcisolem  14966  yonffthlem  15084  gsumpropd2lem  15496  gsumws1  15508  idghm  15753  ghmf1o  15767  symgval  15875  symgbas  15876  elsymgbas  15878  symgbasf  15880  symgbasfi  15882  symg1bas  15892  symggrp  15896  symgid  15897  lactghmga  15900  symgfixf1  15934  f1omvdmvd  15940  f1omvdconj  15943  f1omvdco2  15945  pmtrfconj  15963  symggen  15967  pmtrdifellem1  15973  pmtrdifellem2  15974  psgnunilem1  15990  gsumval3eu  16372  gsumval3OLD  16373  gsumval3lem1  16374  gsumval3  16376  gsumzf1o  16382  gsumzf1oOLD  16385  gsumconst  16417  gsumsub  16437  gsumsubOLD  16438  gsumcom2  16455  dprdfsub  16499  dprdfsubOLD  16506  dprdf1o  16517  dprdsn  16521  ablfaclem2  16575  srngcl  16918  lmhmf1o  17104  fidomndrnglem  17355  psrass1lem  17424  psrnegcl  17444  psrlinv  17445  coe1f2  17640  coe1add  17693  evls1rhmlem  17731  evl1sca  17743  pf1ind  17764  gsumfsum  17854  zntoslem  17964  frgpcyg  17981  islinds2  18217  lindsmm  18232  mdetleib2  18374  mdetrsca  18385  mdetralt  18389  mdetunilem7  18399  mdetunilem9  18401  ssidcn  18834  hausdiag  19193  hmphdis  19344  indishmph  19346  cmphaushmeo  19348  ordthmeolem  19349  txhmeo  19351  pt1hmeo  19354  qtopf1  19364  ufldom  19510  symgtgp  19647  tsmsf1o  19694  iducn  19833  imasdsf1olem  19923  xpsdsval  19931  imasf1obl  20038  icchmeo  20488  iccpnfcnv  20491  xrhmeo  20493  cnheiborlem  20501  ovolctb  20948  ovoliunlem1  20960  ovoliunlem2  20961  iunmbl2  21013  dyadmbl  21055  vitalilem2  21064  vitalilem3  21065  vitalilem4  21066  vitalilem5  21067  mbfid  21089  dvid  21367  dvexp  21402  dvcnvlem  21423  dvcnv  21424  dvcnvrelem2  21465  dvcnvre  21466  efcvx  21889  reefgim  21890  efif1olem4  21976  eff1olem  21979  logrncl  21994  relogcl  22002  dvrelog  22057  relogcn  22058  logcn  22067  logf1o2  22070  dvlog  22071  dvlog2  22073  advlog  22074  advlogexp  22075  logtayl  22080  logccv  22083  dvcxp1  22155  loglesqr  22171  asinrebnd  22271  dvatan  22305  efrlim  22338  amgmlem  22358  wilthlem2  22382  wilthlem3  22383  sqff1o  22495  lgsqrlem4  22658  logdivsum  22757  log2sumbnd  22768  f1otrg  23068  f1otrge  23069  axlowdimlem10  23148  axcontlem5  23165  axcontlem10  23170  umgra1  23211  iseupa  23537  eupatrl  23540  eupa0  23546  eupares  23547  eupap1  23548  eupath2lem3  23551  grposn  23653  ginvsn  23787  dmadjrn  25250  unopnorm  25272  unopadj  25274  unoplin  25275  counop  25276  idcnop  25336  idhmop  25337  unopbd  25370  bracnln  25464  cnvbraval  25465  leopnmid  25493  nmopleid  25494  hmopidmch  25508  hmopidmpj  25509  disjrdx  25884  isoun  25948  fcobij  25976  fcobijfs  25977  abliso  26110  tpr2rico  26294  xrge0iifmhm  26321  xrge0pluscn  26322  rrhre  26399  esumf1o  26456  volmeas  26599  eulerpartgbij  26707  eulerpartlemmf  26710  eulerpartlemgvv  26711  eulerpartlemgf  26714  eulerpartlemgs2  26715  eulerpartlemn  26716  ballotlemsima  26850  lgamcvg2  26993  deranglem  27006  derangsn  27010  derangenlem  27011  subfacp1lem4  27023  subfacp1lem5  27024  subfacp1lem6  27025  cvmfolem  27120  cvmliftlem6  27131  ghomsn  27258  prodeq2ii  27377  prodmolem3  27397  prodmolem2a  27398  fprod  27405  fprodf1o  27410  fprodss  27412  fprodser  27413  fprodcl2lem  27414  fprodmul  27422  fproddiv  27423  fprodn0  27441  mblfinlem2  28382  dvasin  28433  f1ocan1fv  28573  metf1o  28604  ismtyval  28652  isismty  28653  ismtyima  28655  ismtyhmeolem  28656  ismtybndlem  28658  ismrer1  28690  reheibor  28691  rngoisocnv  28740  mapfzcons  29005  mzpresrename  29040  diophrw  29050  eldioph2  29053  diophren  29105  kelac1  29369  imasgim  29408  lnrfg  29428  stoweidlem27  29775  stoweidlem31  29779  stoweidlem39  29787  mat1dimelbas  30790  mat1dimmul  30795  lflnegl  32561  lautset  33566  islaut  33567  lautcl  33571  lautco  33581  pautsetN  33582  ispautN  33583  ldilco  33600  ltrncoidN  33612  ltrncoval  33629  trlcoabs2N  34206  trlcoat  34207  trlcone  34212  cdlemg47a  34218  cdlemg46  34219  cdlemg47  34220  trljco  34224  tgrpgrplem  34233  tendoidcl  34253  tendo0co2  34272  tendo0pl  34275  cdlemi2  34303  cdlemk2  34316  cdlemk4  34318  cdlemk8  34322  cdlemkid2  34408  cdlemk45  34431  cdlemk53b  34440  cdlemk53  34441  cdlemk55a  34443  erng1r  34479  tendocnv  34506  dvalveclem  34510  dva0g  34512  dvhgrp  34592  dvh0g  34596  dvhopN  34601  cdlemn3  34682  cdlemn8  34689  cdlemn9  34690  dihordlem7b  34700  dihopelvalcpre  34733  dihmeetlem1N  34775  dihglblem5apreN  34776  lcfrlem13  35040  hvmapclN  35249  hvmapcl2  35251
  Copyright terms: Public domain W3C validator