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

Theorem f1of 5677
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 5676 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5642 . 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 5453   -1-1->wf1 5454   -1-1-onto->wf1o 5456
This theorem is referenced by:  f1ofn  5678  f1oabexg  5689  f1ompt  5894  fsn  5909  fsnunf  5934  f1ocnvfv1  6017  f1ocnvfv2  6018  f1ocnvdm  6021  fcof1o  6029  fveqf1o  6032  isocnv  6053  isocnv3  6055  isores2  6056  isotr  6059  isofr2  6067  isopolem  6068  isosolem  6070  f1oiso2  6075  weniso  6078  wemoiso  6081  f1ofveu  6587  smoiso  6627  mapsn  7058  f1oen2g  7127  en1  7177  mapen  7274  ac6sfi  7354  domunfican  7382  fiint  7386  supisoex  7479  supiso  7480  ordiso2  7487  ordtypelem10  7499  hartogslem1  7514  unxpwdom2  7559  cantnfle  7629  cantnfp1lem3  7639  cantnflem1b  7645  cantnflem1d  7647  cantnflem1  7648  mapfien  7656  cnfcomlem  7659  cnfcom  7660  cnfcom2lem  7661  cnfcom2  7662  cnfcom3lem  7663  cnfcom3  7664  cnfcom3clem  7665  infxpenlem  7900  infxpenc  7904  infxpenc2lem2  7906  fseqenlem1  7910  acndom  7937  acndom2  7940  infpwfien  7948  iunfictbso  8000  infmap2  8103  ackbij2lem2  8125  infpssrlem3  8190  infpssrlem4  8191  fin23lem30  8227  isf32lem6  8243  isf32lem7  8244  isf32lem8  8245  enfin1ai  8269  axcc3  8323  axcclem  8342  ttukeylem7  8400  fpwwe2lem6  8515  fpwwe2lem7  8516  fpwwe2lem9  8518  canthp1lem2  8533  canthp1  8534  pwfseqlem4a  8541  pwfseqlem5  8543  dfle2  10745  axdc4uzlem  11326  seqf1olem1  11367  seqf1olem2  11368  seqf1o  11369  hashkf  11625  hasheqf1oi  11640  hashcl  11644  hashgadd  11656  hashfacen  11708  hashf1lem1  11709  fz1isolem  11715  seqcoll  11717  seqcoll2  11718  s1cl  11760  cnrecnv  11975  sumeq2ii  12492  summolem3  12513  summolem2a  12514  fsum  12519  fsumf1o  12522  fsumss  12524  fsumcl2lem  12530  fsumadd  12537  fsummulc2  12572  fsumrelem  12591  ackbijnn  12612  sadcaddlem  12974  sadadd2lem  12976  sadadd3  12978  sadaddlem  12983  sadasslem  12987  sadeq  12989  phimullem  13173  eulerthlem1  13175  eulerthlem2  13176  unbenlem  13281  vdwlem8  13361  0ram  13393  wunndx  13490  xpsaddlem  13805  xpsvsca  13809  xpsle  13811  idfucl  14083  setccatid  14244  setcinv  14250  catcisolem  14266  yonffthlem  14384  gsumws1  14790  idghm  15026  ghmf1o  15040  symgval  15099  symgbas  15100  elsymgbas  15102  symggrp  15108  symgid  15109  lactghmga  15112  gsumval3eu  15518  gsumval3  15519  gsumzf1o  15524  gsumconst  15537  gsumsub  15547  gsumcom2  15554  dprdfsub  15584  dprdf1o  15595  dprdsn  15599  ablfaclem2  15649  srngcl  15948  lmhmf1o  16127  fidomndrnglem  16371  psrass1lem  16447  psrnegcl  16465  psrlinv  16466  coe1f2  16612  coe1add  16662  gsumfsum  16771  zntoslem  16842  frgpcyg  16859  ssidcn  17324  hausdiag  17682  hmphdis  17833  indishmph  17835  cmphaushmeo  17837  ordthmeolem  17838  txhmeo  17840  pt1hmeo  17843  qtopf1  17853  ufldom  17999  symgtgp  18136  tsmsf1o  18179  iducn  18318  imasdsf1olem  18408  xpsdsval  18416  imasf1obl  18523  icchmeo  18971  iccpnfcnv  18974  xrhmeo  18976  cnheiborlem  18984  ovolctb  19391  ovoliunlem1  19403  ovoliunlem2  19404  iunmbl2  19456  dyadmbl  19497  vitalilem2  19506  vitalilem3  19507  vitalilem4  19508  vitalilem5  19509  mbfid  19531  dvid  19809  dvexp  19844  dvcnvlem  19865  dvcnv  19866  dvcnvrelem2  19907  dvcnvre  19908  evl1rhm  19954  evl1sca  19955  pf1ind  19980  efcvx  20370  reefgim  20371  efif1olem4  20452  eff1olem  20455  logrncl  20470  relogcl  20478  dvrelog  20533  relogcn  20534  logcn  20543  logf1o2  20546  dvlog  20547  dvlog2  20549  advlog  20550  advlogexp  20551  logtayl  20556  logccv  20559  dvcxp1  20631  loglesqr  20647  asinrebnd  20746  dvatan  20780  efrlim  20813  amgmlem  20833  wilthlem2  20857  wilthlem3  20858  sqff1o  20970  lgsqrlem4  21133  logdivsum  21232  log2sumbnd  21243  umgra1  21366  iseupa  21692  eupatrl  21695  eupa0  21701  eupares  21702  eupap1  21703  eupath2lem3  21706  grposn  21808  ginvsn  21942  dmadjrn  23403  unopnorm  23425  unopadj  23427  unoplin  23428  counop  23429  idcnop  23489  idhmop  23490  unopbd  23523  bracnln  23617  cnvbraval  23618  leopnmid  23646  nmopleid  23647  hmopidmch  23661  hmopidmpj  23662  disjrdx  24036  isoun  24094  gsumpropd2lem  24225  tpr2rico  24315  xrge0iifmhm  24330  xrge0pluscn  24331  rrhre  24392  esumf1o  24450  volmeas  24592  ballotlemsima  24778  lgamcvg2  24844  deranglem  24857  derangsn  24861  derangenlem  24862  subfacp1lem4  24874  subfacp1lem5  24875  subfacp1lem6  24876  cvmfolem  24971  cvmliftlem6  24982  ghomsn  25104  prodeq2ii  25244  prodmolem3  25264  prodmolem2a  25265  fprod  25272  fprodf1o  25277  fprodss  25279  fprodser  25280  fprodcl2lem  25281  fprodmul  25289  fproddiv  25290  fprodn0  25308  axlowdimlem10  25895  axcontlem5  25912  axcontlem10  25917  mblfinlem2  26256  dvreasin  26304  f1ocan1fv  26442  metf1o  26475  ismtyval  26523  isismty  26524  ismtyima  26526  ismtyhmeolem  26527  ismtybndlem  26529  ismrer1  26561  reheibor  26562  rngoisocnv  26611  ralxpmap  26756  mapfzcons  26786  mzpresrename  26821  diophrw  26831  eldioph2  26834  diophren  26888  kelac1  27152  enfixsn  27248  imasgim  27255  islinds2  27274  lindsmm  27289  lnrfg  27314  f1omvdmvd  27377  f1omvdconj  27380  f1omvdco2  27382  pmtrfconj  27398  symggen  27402  psgnunilem1  27407  stoweidlem27  27766  stoweidlem31  27770  stoweidlem39  27778  lflnegl  29948  lautset  30953  islaut  30954  lautcl  30958  lautco  30968  pautsetN  30969  ispautN  30970  ldilco  30987  ltrncoidN  30999  ltrncoval  31016  trlcoabs2N  31593  trlcoat  31594  trlcone  31599  cdlemg47a  31605  cdlemg46  31606  cdlemg47  31607  trljco  31611  tgrpgrplem  31620  tendoidcl  31640  tendo0co2  31659  tendo0pl  31662  cdlemi2  31690  cdlemk2  31703  cdlemk4  31705  cdlemk8  31709  cdlemkid2  31795  cdlemk45  31818  cdlemk53b  31827  cdlemk53  31828  cdlemk55a  31830  erng1r  31866  tendocnv  31893  dvalveclem  31897  dva0g  31899  dvhgrp  31979  dvh0g  31983  dvhopN  31988  cdlemn3  32069  cdlemn8  32076  cdlemn9  32077  dihordlem7b  32087  dihopelvalcpre  32120  dihmeetlem1N  32162  dihglblem5apreN  32163  lcfrlem13  32427  hvmapclN  32636  hvmapcl2  32638
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 179  df-an 362  df-f1 5462  df-f1o 5464
  Copyright terms: Public domain W3C validator