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

Theorem f1of 5658
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 5657 . 2
2 f1f 5623 . 2
31, 2syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  -->wf 5434  -1-1->wf1 5435  -1-1-onto->wf1o 5437
This theorem is referenced by:  f1ofn  5659  f1ompt  5881  f1oresrab  5890  fsn  5896  fsnunf  5931  f1ocnvfv1  5995  f1ocnvfv2  5996  f1ocnvdm  5999  fcof1o  6007  fveqf1o  6010  isocnv  6031  isocnv3  6033  isores2  6034  isotr  6037  isofr2  6045  isopolem  6046  isosolem  6048  f1oiso2  6053  weniso  6055  f1ofveu  6097  f1oabexg  6543  wemoiso  6568  smoiso  6786  mapsn  7218  f1oen2g  7288  en1  7338  mapen  7436  ac6sfi  7517  domunfican  7545  fiint  7549  supisoex  7643  supiso  7644  ordiso2  7651  ordtypelem10  7663  hartogslem1  7678  unxpwdom2  7723  cantnfle  7793  cantnfp1lem3  7803  cantnflem1b  7809  cantnflem1d  7811  cantnflem1  7812  mapfien  7820  cnfcomlem  7823  cnfcom  7824  cnfcom2lem  7825  cnfcom2  7826  cnfcom3lem  7827  cnfcom3  7828  cnfcom3clem  7829  infxpenlem  8066  infxpenc  8070  infxpenc2lem2  8072  fseqenlem1  8076  acndom  8103  acndom2  8106  infpwfien  8114  iunfictbso  8166  infmap2  8269  ackbij2lem2  8291  infpssrlem3  8356  infpssrlem4  8357  fin23lem30  8393  isf32lem6  8409  isf32lem7  8410  isf32lem8  8411  enfin1ai  8435  axcc3  8489  axcclem  8508  ttukeylem7  8566  fpwwe2lem6  8681  fpwwe2lem7  8682  fpwwe2lem9  8684  canthp1lem2  8699  canthp1  8700  pwfseqlem4a  8707  pwfseqlem5  8709  dfle2  10988  axdc4uzlem  11653  seqf1olem1  11694  seqf1olem2  11695  seqf1o  11696  hashkf  11954  hasheqf1oi  11971  hashcl  11975  hashgadd  11989  hashfacen  12054  hashf1lem1  12055  fz1isolem  12061  seqcoll  12063  seqcoll2  12064  snopiswrd  12090  cnrecnv  12501  sumeq2ii  13018  summolem3  13039  summolem2a  13040  fsum  13045  fsumf1o  13048  fsumss  13050  fsumcl2lem  13056  fsumadd  13063  fsummulc2  13098  fsumrelem  13117  ackbijnn  13138  sadcaddlem  13500  sadadd2lem  13502  sadadd3  13504  sadaddlem  13509  sadasslem  13513  sadeq  13515  phimullem  13701  eulerthlem1  13703  eulerthlem2  13704  unbenlem  13816  vdwlem8  13896  0ram  13928  wunndx  14037  xpsaddlem  14354  xpsvsca  14358  xpsle  14360  idfucl  14632  setccatid  14793  setcinv  14799  catcisolem  14815  yonffthlem  14933  gsumws1  15355  idghm  15592  ghmf1o  15606  symgval  15665  symgbas  15666  elsymgbas  15668  symgbasf  15670  symgbasfi  15672  symg1bas  15682  symggrp  15686  symgid  15687  lactghmga  15690  symgfixf1  15719  gsumval3eu  16123  gsumval3  16124  gsumzf1o  16129  gsumconst  16142  gsumsub  16152  gsumcom2  16164  dprdfsub  16194  dprdf1o  16205  dprdsn  16209  ablfaclem2  16259  srngcl  16559  lmhmf1o  16741  fidomndrnglem  16991  psrass1lem  17067  psrnegcl  17085  psrlinv  17086  coe1f2  17232  coe1add  17282  gsumfsum  17391  zntoslem  17462  frgpcyg  17479  f1omvdmvd  17600  f1omvdconj  17603  f1omvdco2  17605  pmtrfconj  17622  symggen  17626  pmtrdifellem1  17629  pmtrdifellem2  17630  psgnunilem1  17646  mdetleib2  17871  mdetf  17878  mdetrlin  17881  mdetrsca  17882  mdetralt  17886  mdetunilem7  17896  mdetunilem9  17898  ssidcn  18333  hausdiag  18692  hmphdis  18843  indishmph  18845  cmphaushmeo  18847  ordthmeolem  18848  txhmeo  18850  pt1hmeo  18853  qtopf1  18863  ufldom  19009  symgtgp  19146  tsmsf1o  19189  iducn  19328  imasdsf1olem  19418  xpsdsval  19426  imasf1obl  19533  icchmeo  19981  iccpnfcnv  19984  xrhmeo  19986  cnheiborlem  19994  ovolctb  20401  ovoliunlem1  20413  ovoliunlem2  20414  iunmbl2  20466  dyadmbl  20507  vitalilem2  20516  vitalilem3  20517  vitalilem4  20518  vitalilem5  20519  mbfid  20541  dvid  20819  dvexp  20854  dvcnvlem  20875  dvcnv  20876  dvcnvrelem2  20917  dvcnvre  20918  evl1rhm  20964  evl1sca  20965  pf1ind  20990  efcvx  21380  reefgim  21381  efif1olem4  21467  eff1olem  21470  logrncl  21485  relogcl  21493  dvrelog  21548  relogcn  21549  logcn  21558  logf1o2  21561  dvlog  21562  dvlog2  21564  advlog  21565  advlogexp  21566  logtayl  21571  logccv  21574  dvcxp1  21646  loglesqr  21662  asinrebnd  21762  dvatan  21796  efrlim  21829  amgmlem  21849  wilthlem2  21873  wilthlem3  21874  sqff1o  21986  lgsqrlem4  22149  logdivsum  22248  log2sumbnd  22259  umgra1  22382  iseupa  22708  eupatrl  22711  eupa0  22717  eupares  22718  eupap1  22719  eupath2lem3  22722  grposn  22824  ginvsn  22958  dmadjrn  24421  unopnorm  24443  unopadj  24445  unoplin  24446  counop  24447  idcnop  24507  idhmop  24508  unopbd  24541  bracnln  24635  cnvbraval  24636  leopnmid  24664  nmopleid  24665  hmopidmch  24679  hmopidmpj  24680  disjrdx  25061  isoun  25127  fcobij  25155  fcobijfs  25156  abliso  25291  gsumpropd2lem  25401  tpr2rico  25521  xrge0iifmhm  25548  xrge0pluscn  25549  rrhre  25627  esumf1o  25684  volmeas  25827  eulerpartgbij  25929  eulerpartlemmf  25932  eulerpartlemgvv  25933  eulerpartlemgf  25936  eulerpartlemgs2  25937  eulerpartlemn  25938  ballotlemsima  26048  lgamcvg2  26187  deranglem  26200  derangsn  26204  derangenlem  26205  subfacp1lem4  26217  subfacp1lem5  26218  subfacp1lem6  26219  cvmfolem  26314  cvmliftlem6  26325  ghomsn  26447  prodeq2ii  26578  prodmolem3  26598  prodmolem2a  26599  fprod  26606  fprodf1o  26611  fprodss  26613  fprodser  26614  fprodcl2lem  26615  fprodmul  26623  fproddiv  26624  fprodn0  26642  axlowdimlem10  27229  axcontlem5  27246  axcontlem10  27251  mblfinlem2  27609  dvasin  27660  f1ocan1fv  27800  metf1o  27833  ismtyval  27881  isismty  27882  ismtyima  27884  ismtyhmeolem  27885  ismtybndlem  27887  ismrer1  27919  reheibor  27920  rngoisocnv  27969  ralxpmap  28176  mapfzcons  28201  mzpresrename  28235  diophrw  28245  eldioph2  28248  diophren  28300  kelac1  28564  enfixsn  28597  imasgim  28604  islinds2  28623  lindsmm  28638  lnrfg  28663  stoweidlem27  29001  stoweidlem31  29005  stoweidlem39  29013  lflnegl  31424  lautset  32429  islaut  32430  lautcl  32434  lautco  32444  pautsetN  32445  ispautN  32446  ldilco  32463  ltrncoidN  32475  ltrncoval  32492  trlcoabs2N  33069  trlcoat  33070  trlcone  33075  cdlemg47a  33081  cdlemg46  33082  cdlemg47  33083  trljco  33087  tgrpgrplem  33096  tendoidcl  33116  tendo0co2  33135  tendo0pl  33138  cdlemi2  33166  cdlemk2  33179  cdlemk4  33181  cdlemk8  33185  cdlemkid2  33271  cdlemk45  33294  cdlemk53b  33303  cdlemk53  33304  cdlemk55a  33306  erng1r  33342  tendocnv  33369  dvalveclem  33373  dva0g  33375  dvhgrp  33455  dvh0g  33459  dvhopN  33464  cdlemn3  33545  cdlemn8  33552  cdlemn9  33553  dihordlem7b  33563  dihopelvalcpre  33596  dihmeetlem1N  33638  dihglblem5apreN  33639  lcfrlem13  33903  hvmapclN  34112  hvmapcl2  34114
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 5443  df-f1o 5445
  Copyright terms: Public domain W3C validator