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

Theorem f1of 5635
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 5634 . 2
2 f1f 5600 . 2
31, 2syl 16 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  -->wf 5413  -1-1->wf1 5414  -1-1-onto->wf1o 5416
This theorem is referenced by:  f1ofn  5636  f1ompt  5853  f1oresrab  5862  fsn  5868  fsnunf  5896  f1ocnvfv1  5959  f1ocnvfv2  5960  f1ocnvdm  5963  fcof1o  5971  fveqf1o  5974  isocnv  5995  isocnv3  5997  isores2  5998  isotr  6001  isofr2  6009  isopolem  6010  isosolem  6012  f1oiso2  6017  weniso  6019  f1ofveu  6061  f1oabexg  6498  wemoiso  6523  smoiso  6736  mapsn  7167  f1oen2g  7236  en1  7286  mapen  7383  ac6sfi  7463  domunfican  7491  fiint  7495  supisoex  7588  supiso  7589  ordiso2  7596  ordtypelem10  7608  hartogslem1  7623  unxpwdom2  7668  cantnfle  7738  cantnfp1lem3  7748  cantnflem1b  7754  cantnflem1d  7756  cantnflem1  7757  mapfien  7765  cnfcomlem  7768  cnfcom  7769  cnfcom2lem  7770  cnfcom2  7771  cnfcom3lem  7772  cnfcom3  7773  cnfcom3clem  7774  infxpenlem  8009  infxpenc  8013  infxpenc2lem2  8015  fseqenlem1  8019  acndom  8046  acndom2  8049  infpwfien  8057  iunfictbso  8109  infmap2  8212  ackbij2lem2  8234  infpssrlem3  8299  infpssrlem4  8300  fin23lem30  8336  isf32lem6  8352  isf32lem7  8353  isf32lem8  8354  enfin1ai  8378  axcc3  8432  axcclem  8451  ttukeylem7  8509  fpwwe2lem6  8624  fpwwe2lem7  8625  fpwwe2lem9  8627  canthp1lem2  8642  canthp1  8643  pwfseqlem4a  8650  pwfseqlem5  8652  dfle2  10931  axdc4uzlem  11596  seqf1olem1  11637  seqf1olem2  11638  seqf1o  11639  hashkf  11897  hasheqf1oi  11914  hashcl  11918  hashgadd  11932  hashfacen  11994  hashf1lem1  11995  fz1isolem  12001  seqcoll  12003  seqcoll2  12004  snopiswrd  12030  cnrecnv  12440  sumeq2ii  12957  summolem3  12978  summolem2a  12979  fsum  12984  fsumf1o  12987  fsumss  12989  fsumcl2lem  12995  fsumadd  13002  fsummulc2  13037  fsumrelem  13056  ackbijnn  13077  sadcaddlem  13439  sadadd2lem  13441  sadadd3  13443  sadaddlem  13448  sadasslem  13452  sadeq  13454  phimullem  13640  eulerthlem1  13642  eulerthlem2  13643  unbenlem  13755  vdwlem8  13835  0ram  13867  wunndx  13976  xpsaddlem  14291  xpsvsca  14295  xpsle  14297  idfucl  14569  setccatid  14730  setcinv  14736  catcisolem  14752  yonffthlem  14870  gsumws1  15288  idghm  15524  ghmf1o  15538  symgval  15597  symgbas  15598  elsymgbas  15600  symggrp  15606  symgid  15607  lactghmga  15610  gsumval3eu  16016  gsumval3  16017  gsumzf1o  16022  gsumconst  16035  gsumsub  16045  gsumcom2  16052  dprdfsub  16082  dprdf1o  16093  dprdsn  16097  ablfaclem2  16147  srngcl  16446  lmhmf1o  16625  fidomndrnglem  16869  psrass1lem  16945  psrnegcl  16963  psrlinv  16964  coe1f2  17110  coe1add  17160  gsumfsum  17269  zntoslem  17340  frgpcyg  17357  ssidcn  17822  hausdiag  18181  hmphdis  18332  indishmph  18334  cmphaushmeo  18336  ordthmeolem  18337  txhmeo  18339  pt1hmeo  18342  qtopf1  18352  ufldom  18498  symgtgp  18635  tsmsf1o  18678  iducn  18817  imasdsf1olem  18907  xpsdsval  18915  imasf1obl  19022  icchmeo  19470  iccpnfcnv  19473  xrhmeo  19475  cnheiborlem  19483  ovolctb  19890  ovoliunlem1  19902  ovoliunlem2  19903  iunmbl2  19955  dyadmbl  19996  vitalilem2  20005  vitalilem3  20006  vitalilem4  20007  vitalilem5  20008  mbfid  20030  dvid  20308  dvexp  20343  dvcnvlem  20364  dvcnv  20365  dvcnvrelem2  20406  dvcnvre  20407  evl1rhm  20453  evl1sca  20454  pf1ind  20479  efcvx  20869  reefgim  20870  efif1olem4  20956  eff1olem  20959  logrncl  20974  relogcl  20982  dvrelog  21037  relogcn  21038  logcn  21047  logf1o2  21050  dvlog  21051  dvlog2  21053  advlog  21054  advlogexp  21055  logtayl  21060  logccv  21063  dvcxp1  21135  loglesqr  21151  asinrebnd  21250  dvatan  21284  efrlim  21317  amgmlem  21337  wilthlem2  21361  wilthlem3  21362  sqff1o  21474  lgsqrlem4  21637  logdivsum  21736  log2sumbnd  21747  umgra1  21870  iseupa  22196  eupatrl  22199  eupa0  22205  eupares  22206  eupap1  22207  eupath2lem3  22210  grposn  22312  ginvsn  22446  dmadjrn  23909  unopnorm  23931  unopadj  23933  unoplin  23934  counop  23935  idcnop  23995  idhmop  23996  unopbd  24029  bracnln  24123  cnvbraval  24124  leopnmid  24152  nmopleid  24153  hmopidmch  24167  hmopidmpj  24168  disjrdx  24552  isoun  24618  fcobij  24646  fcobijfs  24647  abliso  24782  gsumpropd2lem  24892  tpr2rico  25012  xrge0iifmhm  25039  xrge0pluscn  25040  rrhre  25118  esumf1o  25175  volmeas  25318  eulerpartgbij  25420  eulerpartlemmf  25423  eulerpartlemgvv  25424  eulerpartlemgf  25427  eulerpartlemgs2  25428  eulerpartlemn  25429  ballotlemsima  25539  lgamcvg2  25678  deranglem  25691  derangsn  25695  derangenlem  25696  subfacp1lem4  25708  subfacp1lem5  25709  subfacp1lem6  25710  cvmfolem  25805  cvmliftlem6  25816  ghomsn  25938  prodeq2ii  26069  prodmolem3  26089  prodmolem2a  26090  fprod  26097  fprodf1o  26102  fprodss  26104  fprodser  26105  fprodcl2lem  26106  fprodmul  26114  fproddiv  26115  fprodn0  26133  axlowdimlem10  26720  axcontlem5  26737  axcontlem10  26742  mblfinlem2  27100  dvasin  27151  f1ocan1fv  27291  metf1o  27324  ismtyval  27372  isismty  27373  ismtyima  27375  ismtyhmeolem  27376  ismtybndlem  27378  ismrer1  27410  reheibor  27411  rngoisocnv  27460  ralxpmap  27673  mapfzcons  27703  mzpresrename  27738  diophrw  27748  eldioph2  27751  diophren  27803  kelac1  28067  enfixsn  28163  imasgim  28170  islinds2  28189  lindsmm  28204  lnrfg  28229  f1omvdmvd  28292  f1omvdconj  28295  f1omvdco2  28297  pmtrfconj  28313  symggen  28317  psgnunilem1  28322  stoweidlem27  28676  stoweidlem31  28680  stoweidlem39  28688  symg1bas  29597  m2detleiblem3a  29616  lflnegl  31147  lautset  32152  islaut  32153  lautcl  32157  lautco  32167  pautsetN  32168  ispautN  32169  ldilco  32186  ltrncoidN  32198  ltrncoval  32215  trlcoabs2N  32792  trlcoat  32793  trlcone  32798  cdlemg47a  32804  cdlemg46  32805  cdlemg47  32806  trljco  32810  tgrpgrplem  32819  tendoidcl  32839  tendo0co2  32858  tendo0pl  32861  cdlemi2  32889  cdlemk2  32902  cdlemk4  32904  cdlemk8  32908  cdlemkid2  32994  cdlemk45  33017  cdlemk53b  33026  cdlemk53  33027  cdlemk55a  33029  erng1r  33065  tendocnv  33092  dvalveclem  33096  dva0g  33098  dvhgrp  33178  dvh0g  33182  dvhopN  33187  cdlemn3  33268  cdlemn8  33275  cdlemn9  33276  dihordlem7b  33286  dihopelvalcpre  33319  dihmeetlem1N  33361  dihglblem5apreN  33362  lcfrlem13  33626  hvmapclN  33835  hvmapcl2  33837
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 5422  df-f1o 5424
  Copyright terms: Public domain W3C validator