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

Theorem inss2 3403
Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
inss2  |-  ( A  i^i  B )  C_  B

Proof of Theorem inss2
StepHypRef Expression
1 incom 3374 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3402 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3222 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  difin0  3540  ordin  4438  onfr  4447  ordelinel  4507  relin2  4820  relres  4999  ssrnres  5132  cnvcnv  5142  fnresin2  5375  fresaunres2  5429  ssimaex  5600  exfo  5694  ffvresb  5706  ofrfval  6102  ofval  6103  ofrval  6104  offres  6108  off  6109  ofres  6110  ofco  6113  fnwelem  6246  fnse  6248  tpostpos  6270  smores3  6386  erinxp  6749  pmresg  6811  nnfi  7069  ixpfi2  7170  f1opwfi  7175  dffi2  7192  elfiun  7199  marypha1lem  7202  ordtypelem3  7251  ordtypelem6  7254  ordtypelem7  7255  hartogslem1  7273  unxpwdom  7319  epfrs  7429  tcmin  7442  bnd2  7579  tskwe  7599  r0weon  7656  infxpenlem  7657  fodomfi2  7703  infpwfien  7705  cdainf  7834  ackbij1lem6  7867  ackbij1lem9  7870  ackbij1lem10  7871  ackbij1lem11  7872  ackbij1lem15  7876  ackbij1lem16  7877  ackbij1lem18  7879  ackbij1b  7881  sdom2en01  7944  fin23lem26  7967  fin23lem13  7974  isfin1-3  8028  fin56  8035  fin1a2lem9  8050  ttukeylem6  8157  brdom3  8169  brdom5  8170  brdom4  8171  fpwwe2lem8  8275  fpwwe2lem9  8276  fpwwe2lem12  8279  fpwwe2  8281  canthwelem  8288  gruima  8440  ingru  8453  gruina  8456  grur1a  8457  ltrelpi  8529  ltrelnq  8566  nqerf  8570  fzfi  11050  rexanuz  11845  limsupgord  11962  limsupcl  11963  limsupgf  11965  limsupgle  11967  rlimres  12048  lo1res  12049  o1of2  12102  o1rlimmul  12108  ackbijnn  12302  bitsinv1  12649  bitsinvp1  12656  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  sadaddlem  12673  sadasslem  12677  sadeq  12679  smuval2  12689  smupval  12695  smueqlem  12697  prmrec  12985  isstruct2  13173  structcnvcnv  13175  ressbasss  13216  ressress  13221  restsspw  13352  pwsle  13407  submre  13523  isacs2  13571  isacs1i  13575  sscres  13716  rescabs  13726  resscat  13742  funcres2c  13791  coffth  13826  rescfth  13827  ressffth  13828  catccatid  13950  catcisolem  13954  catciso  13955  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997  yoniso  14075  isdrs2  14089  isacs3lem  14285  acsinfd  14299  acsdomd  14300  psssdm2  14340  tsrss  14348  sylow2a  14946  lsmmod  15000  frgpnabllem2  15178  subrgpropd  15595  lssacs  15740  sralmod  15955  asplss  16085  ressmplbas  16216  subrgmpl  16220  opsrtoslem2  16242  mplind  16259  ressply1bas  16323  zlpirlem2  16458  zlpirlem3  16459  basdif0  16707  eltg4i  16714  ntrss2  16810  ntrin  16814  isopn3  16819  mreclatdemo  16849  restbas  16905  resttopon  16908  restuni2  16914  restcld  16919  restfpw  16926  ordtrest  16948  subbascn  17000  cnrest2r  17031  cnpresti  17032  cnprest  17033  lmss  17042  cnrmi  17104  restcnrm  17106  resthauslem  17107  fincmp  17136  imacmp  17140  fiuncmp  17147  cmpfi  17151  cnconn  17164  iuncon  17170  clscon  17172  concompclo  17177  1stcrest  17195  subislly  17223  islly2  17226  cldllycmp  17237  hauspwdom  17243  kgeni  17248  llycmpkgen2  17261  1stckgenlem  17264  ptbasfi  17292  txcls  17315  ptclsg  17325  txcnp  17330  ptcnplem  17331  txtube  17350  txcmplem1  17351  txcmplem2  17352  txkgen  17362  xkopt  17365  xkococnlem  17369  txcon  17399  basqtop  17418  tgqtop  17419  kqdisj  17439  kqnrmlem1  17450  kqnrmlem2  17451  nrmhmph  17501  infil  17574  fbasrn  17595  trfg  17602  uzrest  17608  isufil2  17619  fmfnfmlem4  17668  hauspwpwf1  17698  txflf  17717  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem2  17763  tmdgsum2  17795  tsmsres  17842  tsmsxplem1  17851  blres  17993  met2ndci  18084  metrest  18086  tgioo  18318  zdis  18338  reconnlem2  18348  reconn  18349  cnheibor  18469  lebnum  18478  nmoleub2lem3  18612  nmoleub3  18616  cphsqrcl  18636  tchcph  18683  cfilresi  18737  cfilres  18738  caussi  18739  causs  18740  minveclem4b  18811  minveclem4  18812  ovolfcl  18842  ovolfioo  18843  ovolficc  18844  ovolficcss  18845  ovolfsval  18846  ovolfsf  18847  ovollb  18854  ovoliunlem1  18877  ovolicc2lem1  18892  ovolicc2lem2  18893  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2lem5  18896  ovolicc2  18897  nulmbl  18909  voliunlem1  18923  ioombl1lem4  18934  ovolfs2  18942  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem2a  18953  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombllem6  18959  uniioombl  18960  dyadmbllem  18970  dyadmbl  18971  opnmbllem  18972  volcn  18977  volivth  18978  vitalilem2  18980  vitalilem4  18982  mbfadd  19032  mbfsub  19033  i1fima  19049  i1fima2  19050  i1fd  19052  i1fadd  19066  i1fmul  19067  itg1addlem2  19068  itg1addlem4  19070  itg1addlem5  19071  i1fres  19076  mbfmul  19097  itg2cnlem2  19133  bddmulibl  19209  ellimc2  19243  ellimc3  19245  limcflf  19247  limcresi  19251  limciun  19260  dvreslem  19275  dvres2lem  19276  dvres3a  19280  cpnres  19302  dvaddbr  19303  dvmulbr  19304  dvmptres3  19321  lhop1lem  19376  pf1rcl  19448  ig1peu  19573  taylfvallem1  19752  tayl0  19757  rlimcnp2  20277  xrlimcnp  20279  ppisval  20357  chtf  20362  efchtcl  20365  chtge0  20366  ppinprm  20406  chtprm  20407  chtnprm  20408  chtwordi  20410  chtdif  20412  efchtdvds  20413  chtlepsi  20461  chtleppi  20465  pclogsum  20470  chpval2  20473  chpchtsum  20474  chpub  20475  2sqlem8  20627  2sqlem9  20628  chebbnd1lem1  20634  chtppilimlem1  20638  rplogsumlem2  20650  rpvmasumlem  20652  rplogsum  20692  dirith2  20693  issubgo  20986  opidon  21005  chdmm1i  22072  chm0i  22085  ledii  22131  lejdii  22133  pjoml2i  22180  pjoml4i  22182  cmcmlem  22186  cmbr4i  22196  osumcori  22238  pjssmii  22276  mayete3i  22323  mayete3iOLD  22324  riesz4  22660  riesz1  22661  cnlnadjeu  22674  nmopadjlei  22684  pjclem1  22791  pjci  22796  mdbr3  22893  mdbr4  22894  dmdbr2  22899  dmdbr5  22904  ssmd2  22908  mdslj1i  22915  mdslj2i  22916  mdsl1i  22917  mdsl2bi  22919  mdslmd1lem1  22921  mdslmd1lem2  22922  mdslmd2i  22926  csmdsymi  22930  cvexchlem  22964  atomli  22978  atcvat4i  22993  suppss2f  23216  off2  23223  partfun  23255  pnfneige0  23389  lmxrge0  23390  esumcst  23451  esumpcvgval  23461  hasheuni  23468  esumcvg  23469  sigainb  23512  indf1ofs  23624  probdif  23638  probmeasb  23648  cndprob01  23653  conpcon  23781  iccllyscon  23796  cvmsss2  23820  cvmcov2  23821  cvmopnlem  23824  cvmliftmolem2  23828  cvmlift2lem12  23860  nepss  24087  dedekindle  24098  elrn3  24191  dfon2lem4  24213  wfrlem4  24330  frrlem4  24355  domintrefb  25166  toplat  25393  reacomsmgrp1  25446  reacomsmgrp2  25447  reacomsmgrp3  25448  limptlimpr2lem2  25678  lvsovso  25729  tartarmap  25991  inttarcar  26004  cardtar  26007  bsstrs  26249  nbssntrs  26250  trer  26330  neiin  26353  neibastop1  26411  neibastop2lem  26412  topmeet  26416  filnetlem3  26432  heibor1lem  26636  heiborlem1  26638  heiborlem3  26640  heiborlem10  26647  elrfi  26872  elrfirn  26873  fnwe2lem2  27251  aomclem2  27255  lsmfgcl  27275  lmhmfgima  27285  lmhmfgsplit  27287  lmhmlnmsplit  27288  uvcff  27343  hbt  27437  mvdco  27491  acsfn1p  27610  onfrALTlem3  28608  onfrALTlem2  28610  onfrALTlem3VD  28979  onfrALTlem2VD  28981  bnj1293  29165  lshpinN  29801  lcvexchlem1  29846  lcvexchlem5  29850  pmod1i  30659  pmodN  30661  osumcllem7N  30773  pexmidlem4N  30784  dochdmj1  32202  dochexmidlem4  32275  lcfrlem25  32379  mapd1o  32460  mapdin  32474
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator