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

Theorem f1of 5472
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 5471 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5437 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
31, 2syl 15 1  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   -->wf 5251   -1-1->wf1 5252   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1ofn  5473  f1oabexg  5484  f1ompt  5682  fsn  5696  fsnunf  5718  f1ocnvfv1  5792  f1ocnvfv2  5793  f1ocnvdm  5796  fcof1o  5803  fveqf1o  5806  isocnv  5827  isocnv3  5829  isores2  5830  isotr  5833  isofr2  5841  isopolem  5842  isosolem  5844  f1oiso2  5849  weniso  5852  wemoiso  5855  f1ofveu  6339  smoiso  6379  mapsn  6809  f1oen2g  6878  en1  6928  mapen  7025  ac6sfi  7101  domunfican  7129  fiint  7133  supisoex  7222  supiso  7223  ordiso2  7230  ordtypelem10  7242  hartogslem1  7257  unxpwdom2  7302  cantnfle  7372  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  mapfien  7399  cnfcomlem  7402  cnfcom  7403  cnfcom2lem  7404  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  cnfcom3clem  7408  infxpenlem  7641  infxpenc  7645  infxpenc2lem2  7647  fseqenlem1  7651  acndom  7678  acndom2  7681  infpwfien  7689  iunfictbso  7741  infmap2  7844  ackbij2lem2  7866  infpssrlem3  7931  infpssrlem4  7932  fin23lem30  7968  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  enfin1ai  8010  axcc3  8064  axcclem  8083  ttukeylem7  8142  fpwwe2lem6  8257  fpwwe2lem7  8258  fpwwe2lem9  8260  canthp1lem2  8275  canthp1  8276  pwfseqlem4a  8283  pwfseqlem5  8285  dfle2  10481  axdc4uzlem  11044  seqf1olem1  11085  seqf1olem2  11086  seqf1o  11087  hashkf  11339  hashcl  11350  hashgadd  11359  hashfacen  11392  hashf1lem1  11393  fz1isolem  11399  seqcoll  11401  seqcoll2  11402  s1cl  11441  cnrecnv  11650  sumeq2ii  12166  summolem3  12187  summolem2a  12188  fsum  12193  fsumf1o  12196  fsumss  12198  fsumcl2lem  12204  fsumadd  12211  fsummulc2  12246  fsumrelem  12265  ackbijnn  12286  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  phimullem  12847  eulerthlem1  12849  eulerthlem2  12850  unbenlem  12955  vdwlem8  13035  0ram  13067  wunndx  13164  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  idfucl  13755  setccatid  13916  setcinv  13922  catcisolem  13938  yonffthlem  14056  gsumws1  14462  idghm  14698  ghmf1o  14712  symgval  14771  symgbas  14772  elsymgbas  14774  symggrp  14780  symgid  14781  lactghmga  14784  gsumval3eu  15190  gsumval3  15191  gsumzf1o  15196  gsumconst  15209  gsumsub  15219  gsumcom2  15226  dprdfsub  15256  dprdf1o  15267  dprdsn  15271  ablfaclem2  15321  srngcl  15620  lmhmf1o  15803  fidomndrnglem  16047  psrass1lem  16123  psrnegcl  16141  psrlinv  16142  coe1f2  16290  coe1add  16341  gsumfsum  16439  zntoslem  16510  frgpcyg  16527  ssidcn  16985  hausdiag  17339  hmphdis  17487  indishmph  17489  cmphaushmeo  17491  ordthmeolem  17492  txhmeo  17494  pt1hmeo  17497  qtopf1  17507  ufldom  17657  symgtgp  17784  tsmsf1o  17827  imasdsf1olem  17937  xpsdsval  17945  imasf1obl  18034  icchmeo  18439  iccpnfcnv  18442  xrhmeo  18444  cnheiborlem  18452  ovolctb  18849  ovoliunlem1  18861  ovoliunlem2  18862  iunmbl2  18914  dyadmbl  18955  vitalilem2  18964  vitalilem3  18965  vitalilem4  18966  vitalilem5  18967  mbfid  18991  dvid  19267  dvexp  19302  dvcnvlem  19323  dvcnv  19324  dvcnvrelem2  19365  dvcnvre  19366  evl1rhm  19412  evl1sca  19413  pf1ind  19438  efcvx  19825  reefgim  19826  resinf1o  19898  efif1olem4  19907  eff1olem  19910  logrncl  19925  relogcl  19932  dvrelog  19984  relogcn  19985  logcn  19994  logf1o2  19997  dvlog  19998  dvlog2  20000  advlog  20001  advlogexp  20002  logtayl  20007  logccv  20010  dvcxp1  20082  loglesqr  20098  asinrebnd  20197  dvatan  20231  efrlim  20264  amgmlem  20284  wilthlem2  20307  wilthlem3  20308  sqff1o  20420  lgsqrlem4  20583  logdivsum  20682  log2sumbnd  20693  grposn  20882  ginvsn  21016  dmadjrn  22475  unopnorm  22497  unopadj  22499  unoplin  22500  counop  22501  idcnop  22561  idhmop  22562  unopbd  22595  bracnln  22689  cnvbraval  22690  leopnmid  22718  nmopleid  22719  hmopidmch  22733  hmopidmpj  22734  ballotlemsima  23074  ballotlem7  23094  isoun  23242  tpr2rico  23296  xrge0iifmhm  23321  xrge0pluscn  23322  disjrdx  23370  gsumpropd2lem  23379  esumf1o  23429  deranglem  23697  derangsn  23701  derangenlem  23702  subfacp1lem4  23714  subfacp1lem5  23715  subfacp1lem6  23716  cvmfolem  23810  cvmliftlem6  23821  umgra1  23878  iseupa  23881  eupa0  23898  eupares  23899  eupap1  23900  eupath2lem3  23903  ghomsn  23995  axlowdimlem10  24579  axcontlem5  24596  axcontlem10  24601  dvreasin  24923  scprefat  25071  cbicp  25166  isoriso  25212  oriso  25214  dispos  25287  hmeogrpi  25536  1alg  25722  idfisf  25841  idsubfun  25858  idcatfun  25941  1iskle  25989  phckle  26027  psckle  26028  pgapspf  26052  f1ocan1fv  26394  metf1o  26469  ismtyval  26524  isismty  26525  ismtyima  26527  ismtyhmeolem  26528  ismtybndlem  26530  ismrer1  26562  reheibor  26563  rngoisocnv  26612  ralxpmap  26761  mapfzcons  26793  mzpresrename  26828  diophrw  26838  eldioph2  26841  diophren  26896  kelac1  27161  enfixsn  27257  imasgim  27264  islinds2  27283  lindsmm  27298  lnrfg  27323  f1omvdmvd  27386  f1omvdconj  27389  f1omvdco2  27391  pmtrfconj  27407  symggen  27411  psgnunilem1  27416  stoweidlem27  27776  stoweidlem31  27780  stoweidlem39  27788  lflnegl  29266  lautset  30271  islaut  30272  lautcl  30276  lautco  30286  pautsetN  30287  ispautN  30288  ldilco  30305  ltrncoidN  30317  ltrncoval  30334  trlcoabs2N  30911  trlcoat  30912  trlcone  30917  cdlemg47a  30923  cdlemg46  30924  cdlemg47  30925  trljco  30929  tgrpgrplem  30938  tendoidcl  30958  tendo0co2  30977  tendo0pl  30980  cdlemi2  31008  cdlemk2  31021  cdlemk4  31023  cdlemk8  31027  cdlemkid2  31113  cdlemk45  31136  cdlemk53b  31145  cdlemk53  31146  cdlemk55a  31148  erng1r  31184  tendocnv  31211  dvalveclem  31215  dva0g  31217  dvhgrp  31297  dvh0g  31301  dvhopN  31306  cdlemn3  31387  cdlemn8  31394  cdlemn9  31395  dihordlem7b  31405  dihopelvalcpre  31438  dihmeetlem1N  31480  dihglblem5apreN  31481  lcfrlem13  31745  hvmapclN  31954  hvmapcl2  31956
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-f1 5260  df-f1o 5262
  Copyright terms: Public domain W3C validator