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

Theorem f1of 5633
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 5632 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5598 . 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 set class
Syntax hints:    -> wi 4   -->wf 5409   -1-1->wf1 5410   -1-1-onto->wf1o 5412
This theorem is referenced by:  f1ofn  5634  f1oabexg  5645  f1ompt  5850  fsn  5865  fsnunf  5890  f1ocnvfv1  5973  f1ocnvfv2  5974  f1ocnvdm  5977  fcof1o  5985  fveqf1o  5988  isocnv  6009  isocnv3  6011  isores2  6012  isotr  6015  isofr2  6023  isopolem  6024  isosolem  6026  f1oiso2  6031  weniso  6034  wemoiso  6037  f1ofveu  6543  smoiso  6583  mapsn  7014  f1oen2g  7083  en1  7133  mapen  7230  ac6sfi  7310  domunfican  7338  fiint  7342  supisoex  7432  supiso  7433  ordiso2  7440  ordtypelem10  7452  hartogslem1  7467  unxpwdom2  7512  cantnfle  7582  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  mapfien  7609  cnfcomlem  7612  cnfcom  7613  cnfcom2lem  7614  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  cnfcom3clem  7618  infxpenlem  7851  infxpenc  7855  infxpenc2lem2  7857  fseqenlem1  7861  acndom  7888  acndom2  7891  infpwfien  7899  iunfictbso  7951  infmap2  8054  ackbij2lem2  8076  infpssrlem3  8141  infpssrlem4  8142  fin23lem30  8178  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  enfin1ai  8220  axcc3  8274  axcclem  8293  ttukeylem7  8351  fpwwe2lem6  8466  fpwwe2lem7  8467  fpwwe2lem9  8469  canthp1lem2  8484  canthp1  8485  pwfseqlem4a  8492  pwfseqlem5  8494  dfle2  10696  axdc4uzlem  11276  seqf1olem1  11317  seqf1olem2  11318  seqf1o  11319  hashkf  11575  hasheqf1oi  11590  hashcl  11594  hashgadd  11606  hashfacen  11658  hashf1lem1  11659  fz1isolem  11665  seqcoll  11667  seqcoll2  11668  s1cl  11710  cnrecnv  11925  sumeq2ii  12442  summolem3  12463  summolem2a  12464  fsum  12469  fsumf1o  12472  fsumss  12474  fsumcl2lem  12480  fsumadd  12487  fsummulc2  12522  fsumrelem  12541  ackbijnn  12562  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  sadasslem  12937  sadeq  12939  phimullem  13123  eulerthlem1  13125  eulerthlem2  13126  unbenlem  13231  vdwlem8  13311  0ram  13343  wunndx  13440  xpsaddlem  13755  xpsvsca  13759  xpsle  13761  idfucl  14033  setccatid  14194  setcinv  14200  catcisolem  14216  yonffthlem  14334  gsumws1  14740  idghm  14976  ghmf1o  14990  symgval  15049  symgbas  15050  elsymgbas  15052  symggrp  15058  symgid  15059  lactghmga  15062  gsumval3eu  15468  gsumval3  15469  gsumzf1o  15474  gsumconst  15487  gsumsub  15497  gsumcom2  15504  dprdfsub  15534  dprdf1o  15545  dprdsn  15549  ablfaclem2  15599  srngcl  15898  lmhmf1o  16077  fidomndrnglem  16321  psrass1lem  16397  psrnegcl  16415  psrlinv  16416  coe1f2  16562  coe1add  16612  gsumfsum  16721  zntoslem  16792  frgpcyg  16809  ssidcn  17273  hausdiag  17630  hmphdis  17781  indishmph  17783  cmphaushmeo  17785  ordthmeolem  17786  txhmeo  17788  pt1hmeo  17791  qtopf1  17801  ufldom  17947  symgtgp  18084  tsmsf1o  18127  iducn  18266  imasdsf1olem  18356  xpsdsval  18364  imasf1obl  18471  icchmeo  18919  iccpnfcnv  18922  xrhmeo  18924  cnheiborlem  18932  ovolctb  19339  ovoliunlem1  19351  ovoliunlem2  19352  iunmbl2  19404  dyadmbl  19445  vitalilem2  19454  vitalilem3  19455  vitalilem4  19456  vitalilem5  19457  mbfid  19481  dvid  19757  dvexp  19792  dvcnvlem  19813  dvcnv  19814  dvcnvrelem2  19855  dvcnvre  19856  evl1rhm  19902  evl1sca  19903  pf1ind  19928  efcvx  20318  reefgim  20319  efif1olem4  20400  eff1olem  20403  logrncl  20418  relogcl  20426  dvrelog  20481  relogcn  20482  logcn  20491  logf1o2  20494  dvlog  20495  dvlog2  20497  advlog  20498  advlogexp  20499  logtayl  20504  logccv  20507  dvcxp1  20579  loglesqr  20595  asinrebnd  20694  dvatan  20728  efrlim  20761  amgmlem  20781  wilthlem2  20805  wilthlem3  20806  sqff1o  20918  lgsqrlem4  21081  logdivsum  21180  log2sumbnd  21191  umgra1  21314  iseupa  21640  eupatrl  21643  eupa0  21649  eupares  21650  eupap1  21651  eupath2lem3  21654  grposn  21756  ginvsn  21890  dmadjrn  23351  unopnorm  23373  unopadj  23375  unoplin  23376  counop  23377  idcnop  23437  idhmop  23438  unopbd  23471  bracnln  23565  cnvbraval  23566  leopnmid  23594  nmopleid  23595  hmopidmch  23609  hmopidmpj  23610  disjrdx  23984  isoun  24042  gsumpropd2lem  24173  tpr2rico  24263  xrge0iifmhm  24278  xrge0pluscn  24279  rrhre  24340  esumf1o  24398  volmeas  24540  ballotlemsima  24726  lgamcvg2  24792  deranglem  24805  derangsn  24809  derangenlem  24810  subfacp1lem4  24822  subfacp1lem5  24823  subfacp1lem6  24824  cvmfolem  24919  cvmliftlem6  24930  ghomsn  25052  prodeq2ii  25192  prodmolem3  25212  prodmolem2a  25213  fprod  25220  fprodf1o  25225  fprodss  25227  fprodser  25228  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodn0  25256  axlowdimlem10  25794  axcontlem5  25811  axcontlem10  25816  mblfinlem  26143  dvreasin  26179  f1ocan1fv  26318  metf1o  26351  ismtyval  26399  isismty  26400  ismtyima  26402  ismtyhmeolem  26403  ismtybndlem  26405  ismrer1  26437  reheibor  26438  rngoisocnv  26487  ralxpmap  26632  mapfzcons  26662  mzpresrename  26697  diophrw  26707  eldioph2  26710  diophren  26764  kelac1  27029  enfixsn  27125  imasgim  27132  islinds2  27151  lindsmm  27166  lnrfg  27191  f1omvdmvd  27254  f1omvdconj  27257  f1omvdco2  27259  pmtrfconj  27275  symggen  27279  psgnunilem1  27284  stoweidlem27  27643  stoweidlem31  27647  stoweidlem39  27655  lflnegl  29559  lautset  30564  islaut  30565  lautcl  30569  lautco  30579  pautsetN  30580  ispautN  30581  ldilco  30598  ltrncoidN  30610  ltrncoval  30627  trlcoabs2N  31204  trlcoat  31205  trlcone  31210  cdlemg47a  31216  cdlemg46  31217  cdlemg47  31218  trljco  31222  tgrpgrplem  31231  tendoidcl  31251  tendo0co2  31270  tendo0pl  31273  cdlemi2  31301  cdlemk2  31314  cdlemk4  31316  cdlemk8  31320  cdlemkid2  31406  cdlemk45  31429  cdlemk53b  31438  cdlemk53  31439  cdlemk55a  31441  erng1r  31477  tendocnv  31504  dvalveclem  31508  dva0g  31510  dvhgrp  31590  dvh0g  31594  dvhopN  31599  cdlemn3  31680  cdlemn8  31687  cdlemn9  31688  dihordlem7b  31698  dihopelvalcpre  31731  dihmeetlem1N  31773  dihglblem5apreN  31774  lcfrlem13  32038  hvmapclN  32247  hvmapcl2  32249
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 178  df-an 361  df-f1 5418  df-f1o 5420
  Copyright terms: Public domain W3C validator