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

Theorem f1of 5721
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 5720 . 2
2 f1f 5686 . 2
31, 2syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  -->wf 5497  -1-1->wf1 5498  -1-1-onto->wf1o 5500
This theorem is referenced by:  f1ofn  5722  f1oabexg  5733  f1ompt  5939  fsn  5954  fsnunf  5979  f1ocnvfv1  6062  f1ocnvfv2  6063  f1ocnvdm  6066  fcof1o  6074  fveqf1o  6077  isocnv  6098  isocnv3  6100  isores2  6101  isotr  6104  isofr2  6112  isopolem  6113  isosolem  6115  f1oiso2  6120  weniso  6123  wemoiso  6126  f1ofveu  6633  smoiso  6673  mapsn  7104  f1oen2g  7173  en1  7223  mapen  7320  ac6sfi  7400  domunfican  7428  fiint  7432  supisoex  7525  supiso  7526  ordiso2  7533  ordtypelem10  7545  hartogslem1  7560  unxpwdom2  7605  cantnfle  7675  cantnfp1lem3  7685  cantnflem1b  7691  cantnflem1d  7693  cantnflem1  7694  mapfien  7702  cnfcomlem  7705  cnfcom  7706  cnfcom2lem  7707  cnfcom2  7708  cnfcom3lem  7709  cnfcom3  7710  cnfcom3clem  7711  infxpenlem  7946  infxpenc  7950  infxpenc2lem2  7952  fseqenlem1  7956  acndom  7983  acndom2  7986  infpwfien  7994  iunfictbso  8046  infmap2  8149  ackbij2lem2  8171  infpssrlem3  8236  infpssrlem4  8237  fin23lem30  8273  isf32lem6  8289  isf32lem7  8290  isf32lem8  8291  enfin1ai  8315  axcc3  8369  axcclem  8388  ttukeylem7  8446  fpwwe2lem6  8561  fpwwe2lem7  8562  fpwwe2lem9  8564  canthp1lem2  8579  canthp1  8580  pwfseqlem4a  8587  pwfseqlem5  8589  dfle2  10791  axdc4uzlem  11372  seqf1olem1  11413  seqf1olem2  11414  seqf1o  11415  hashkf  11671  hasheqf1oi  11686  hashcl  11690  hashgadd  11702  hashfacen  11754  hashf1lem1  11755  fz1isolem  11761  seqcoll  11763  seqcoll2  11764  s1cl  11806  cnrecnv  12021  sumeq2ii  12538  summolem3  12559  summolem2a  12560  fsum  12565  fsumf1o  12568  fsumss  12570  fsumcl2lem  12576  fsumadd  12583  fsummulc2  12618  fsumrelem  12637  ackbijnn  12658  sadcaddlem  13020  sadadd2lem  13022  sadadd3  13024  sadaddlem  13029  sadasslem  13033  sadeq  13035  phimullem  13219  eulerthlem1  13221  eulerthlem2  13222  unbenlem  13327  vdwlem8  13407  0ram  13439  wunndx  13536  xpsaddlem  13851  xpsvsca  13855  xpsle  13857  idfucl  14129  setccatid  14290  setcinv  14296  catcisolem  14312  yonffthlem  14430  gsumws1  14836  idghm  15072  ghmf1o  15086  symgval  15145  symgbas  15146  elsymgbas  15148  symggrp  15154  symgid  15155  lactghmga  15158  gsumval3eu  15564  gsumval3  15565  gsumzf1o  15570  gsumconst  15583  gsumsub  15593  gsumcom2  15600  dprdfsub  15630  dprdf1o  15641  dprdsn  15645  ablfaclem2  15695  srngcl  15994  lmhmf1o  16173  fidomndrnglem  16417  psrass1lem  16493  psrnegcl  16511  psrlinv  16512  coe1f2  16658  coe1add  16708  gsumfsum  16817  zntoslem  16888  frgpcyg  16905  ssidcn  17370  hausdiag  17728  hmphdis  17879  indishmph  17881  cmphaushmeo  17883  ordthmeolem  17884  txhmeo  17886  pt1hmeo  17889  qtopf1  17899  ufldom  18045  symgtgp  18182  tsmsf1o  18225  iducn  18364  imasdsf1olem  18454  xpsdsval  18462  imasf1obl  18569  icchmeo  19017  iccpnfcnv  19020  xrhmeo  19022  cnheiborlem  19030  ovolctb  19437  ovoliunlem1  19449  ovoliunlem2  19450  iunmbl2  19502  dyadmbl  19543  vitalilem2  19552  vitalilem3  19553  vitalilem4  19554  vitalilem5  19555  mbfid  19577  dvid  19855  dvexp  19890  dvcnvlem  19911  dvcnv  19912  dvcnvrelem2  19953  dvcnvre  19954  evl1rhm  20000  evl1sca  20001  pf1ind  20026  efcvx  20416  reefgim  20417  efif1olem4  20498  eff1olem  20501  logrncl  20516  relogcl  20524  dvrelog  20579  relogcn  20580  logcn  20589  logf1o2  20592  dvlog  20593  dvlog2  20595  advlog  20596  advlogexp  20597  logtayl  20602  logccv  20605  dvcxp1  20677  loglesqr  20693  asinrebnd  20792  dvatan  20826  efrlim  20859  amgmlem  20879  wilthlem2  20903  wilthlem3  20904  sqff1o  21016  lgsqrlem4  21179  logdivsum  21278  log2sumbnd  21289  umgra1  21412  iseupa  21738  eupatrl  21741  eupa0  21747  eupares  21748  eupap1  21749  eupath2lem3  21752  grposn  21854  ginvsn  21988  dmadjrn  23449  unopnorm  23471  unopadj  23473  unoplin  23474  counop  23475  idcnop  23535  idhmop  23536  unopbd  23569  bracnln  23663  cnvbraval  23664  leopnmid  23692  nmopleid  23693  hmopidmch  23707  hmopidmpj  23708  disjrdx  24080  isoun  24137  gsumpropd2lem  24269  tpr2rico  24359  xrge0iifmhm  24374  xrge0pluscn  24375  rrhre  24436  esumf1o  24494  volmeas  24636  fcobij  24720  fcobijfs  24721  frabbijd  24722  eulerpartgbij  24758  eulerpartlemmf  24761  eulerpartlemgvv  24762  eulerpartlemgf  24765  eulerpartlemgs2  24766  eulerpartlemn  24767  ballotlemsima  24877  lgamcvg2  24943  deranglem  24956  derangsn  24960  derangenlem  24961  subfacp1lem4  24973  subfacp1lem5  24974  subfacp1lem6  24975  cvmfolem  25070  cvmliftlem6  25081  ghomsn  25203  prodeq2ii  25343  prodmolem3  25363  prodmolem2a  25364  fprod  25371  fprodf1o  25376  fprodss  25378  fprodser  25379  fprodcl2lem  25380  fprodmul  25388  fproddiv  25389  fprodn0  25407  axlowdimlem10  25994  axcontlem5  26011  axcontlem10  26016  mblfinlem2  26353  dvreasin  26401  f1ocan1fv  26539  metf1o  26572  ismtyval  26620  isismty  26621  ismtyima  26623  ismtyhmeolem  26624  ismtybndlem  26626  ismrer1  26658  reheibor  26659  rngoisocnv  26708  ralxpmap  26923  mapfzcons  26953  mzpresrename  26988  diophrw  26998  eldioph2  27001  diophren  27053  kelac1  27317  enfixsn  27413  imasgim  27420  islinds2  27439  lindsmm  27454  lnrfg  27479  f1omvdmvd  27542  f1omvdconj  27545  f1omvdco2  27547  pmtrfconj  27563  symggen  27567  psgnunilem1  27572  stoweidlem27  27930  stoweidlem31  27934  stoweidlem39  27942  lflnegl  30114  lautset  31119  islaut  31120  lautcl  31124  lautco  31134  pautsetN  31135  ispautN  31136  ldilco  31153  ltrncoidN  31165  ltrncoval  31182  trlcoabs2N  31759  trlcoat  31760  trlcone  31765  cdlemg47a  31771  cdlemg46  31772  cdlemg47  31773  trljco  31777  tgrpgrplem  31786  tendoidcl  31806  tendo0co2  31825  tendo0pl  31828  cdlemi2  31856  cdlemk2  31869  cdlemk4  31871  cdlemk8  31875  cdlemkid2  31961  cdlemk45  31984  cdlemk53b  31993  cdlemk53  31994  cdlemk55a  31996  erng1r  32032  tendocnv  32059  dvalveclem  32063  dva0g  32065  dvhgrp  32145  dvh0g  32149  dvhopN  32154  cdlemn3  32235  cdlemn8  32242  cdlemn9  32243  dihordlem7b  32253  dihopelvalcpre  32286  dihmeetlem1N  32328  dihglblem5apreN  32329  lcfrlem13  32593  hvmapclN  32802  hvmapcl2  32804
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 5506  df-f1o 5508
  Copyright terms: Public domain W3C validator