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

Theorem inss2 3390
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 3361 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3389 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3209 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  difin0  3527  ordin  4422  onfr  4431  ordelinel  4491  relin2  4804  relres  4983  ssrnres  5116  cnvcnv  5126  fnresin2  5359  fresaunres2  5413  ssimaex  5584  exfo  5678  ffvresb  5690  ofrfval  6086  ofval  6087  ofrval  6088  offres  6092  off  6093  ofres  6094  ofco  6097  fnwelem  6230  fnse  6232  tpostpos  6254  smores3  6370  erinxp  6733  pmresg  6795  nnfi  7053  ixpfi2  7154  f1opwfi  7159  dffi2  7176  elfiun  7183  marypha1lem  7186  ordtypelem3  7235  ordtypelem6  7238  ordtypelem7  7239  hartogslem1  7257  unxpwdom  7303  epfrs  7413  tcmin  7426  bnd2  7563  tskwe  7583  r0weon  7640  infxpenlem  7641  fodomfi2  7687  infpwfien  7689  cdainf  7818  ackbij1lem6  7851  ackbij1lem9  7854  ackbij1lem10  7855  ackbij1lem11  7856  ackbij1lem15  7860  ackbij1lem16  7861  ackbij1lem18  7863  ackbij1b  7865  sdom2en01  7928  fin23lem26  7951  fin23lem13  7958  isfin1-3  8012  fin56  8019  fin1a2lem9  8034  ttukeylem6  8141  brdom3  8153  brdom5  8154  brdom4  8155  fpwwe2lem8  8259  fpwwe2lem9  8260  fpwwe2lem12  8263  fpwwe2  8265  canthwelem  8272  gruima  8424  ingru  8437  gruina  8440  grur1a  8441  ltrelpi  8513  ltrelnq  8550  nqerf  8554  fzfi  11034  rexanuz  11829  limsupgord  11946  limsupcl  11947  limsupgf  11949  limsupgle  11951  rlimres  12032  lo1res  12033  o1of2  12086  o1rlimmul  12092  ackbijnn  12286  bitsinv1  12633  bitsinvp1  12640  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  smuval2  12673  smupval  12679  smueqlem  12681  prmrec  12969  isstruct2  13157  structcnvcnv  13159  ressbasss  13200  ressress  13205  restsspw  13336  pwsle  13391  submre  13507  isacs2  13555  isacs1i  13559  sscres  13700  rescabs  13710  resscat  13726  funcres2c  13775  coffth  13810  rescfth  13811  ressffth  13812  catccatid  13934  catcisolem  13938  catciso  13939  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  yoniso  14059  isdrs2  14073  isacs3lem  14269  acsinfd  14283  acsdomd  14284  psssdm2  14324  tsrss  14332  sylow2a  14930  lsmmod  14984  frgpnabllem2  15162  subrgpropd  15579  lssacs  15724  sralmod  15939  asplss  16069  ressmplbas  16200  subrgmpl  16204  opsrtoslem2  16226  mplind  16243  ressply1bas  16307  zlpirlem2  16442  zlpirlem3  16443  basdif0  16691  eltg4i  16698  ntrss2  16794  ntrin  16798  isopn3  16803  mreclatdemo  16833  restbas  16889  resttopon  16892  restuni2  16898  restcld  16903  restfpw  16910  ordtrest  16932  subbascn  16984  cnrest2r  17015  cnpresti  17016  cnprest  17017  lmss  17026  cnrmi  17088  restcnrm  17090  resthauslem  17091  fincmp  17120  imacmp  17124  fiuncmp  17131  cmpfi  17135  cnconn  17148  iuncon  17154  clscon  17156  concompclo  17161  1stcrest  17179  subislly  17207  islly2  17210  cldllycmp  17221  hauspwdom  17227  kgeni  17232  llycmpkgen2  17245  1stckgenlem  17248  ptbasfi  17276  txcls  17299  ptclsg  17309  txcnp  17314  ptcnplem  17315  txtube  17334  txcmplem1  17335  txcmplem2  17336  txkgen  17346  xkopt  17349  xkococnlem  17353  txcon  17383  basqtop  17402  tgqtop  17403  kqdisj  17423  kqnrmlem1  17434  kqnrmlem2  17435  nrmhmph  17485  infil  17558  fbasrn  17579  trfg  17586  uzrest  17592  isufil2  17603  fmfnfmlem4  17652  hauspwpwf1  17682  txflf  17701  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem2  17747  tmdgsum2  17779  tsmsres  17826  tsmsxplem1  17835  blres  17977  met2ndci  18068  metrest  18070  tgioo  18302  zdis  18322  reconnlem2  18332  reconn  18333  cnheibor  18453  lebnum  18462  nmoleub2lem3  18596  nmoleub3  18600  cphsqrcl  18620  tchcph  18667  cfilresi  18721  cfilres  18722  caussi  18723  causs  18724  minveclem4b  18795  minveclem4  18796  ovolfcl  18826  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovolfsval  18830  ovolfsf  18831  ovollb  18838  ovoliunlem1  18861  ovolicc2lem1  18876  ovolicc2lem2  18877  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  nulmbl  18893  voliunlem1  18907  ioombl1lem4  18918  ovolfs2  18926  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2a  18937  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombllem6  18943  uniioombl  18944  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  volcn  18961  volivth  18962  vitalilem2  18964  vitalilem4  18966  mbfadd  19016  mbfsub  19017  i1fima  19033  i1fima2  19034  i1fd  19036  i1fadd  19050  i1fmul  19051  itg1addlem2  19052  itg1addlem4  19054  itg1addlem5  19055  i1fres  19060  mbfmul  19081  itg2cnlem2  19117  bddmulibl  19193  ellimc2  19227  ellimc3  19229  limcflf  19231  limcresi  19235  limciun  19244  dvreslem  19259  dvres2lem  19260  dvres3a  19264  cpnres  19286  dvaddbr  19287  dvmulbr  19288  dvmptres3  19305  lhop1lem  19360  pf1rcl  19432  ig1peu  19557  taylfvallem1  19736  tayl0  19741  rlimcnp2  20261  xrlimcnp  20263  ppisval  20341  chtf  20346  efchtcl  20349  chtge0  20350  ppinprm  20390  chtprm  20391  chtnprm  20392  chtwordi  20394  chtdif  20396  efchtdvds  20397  chtlepsi  20445  chtleppi  20449  pclogsum  20454  chpval2  20457  chpchtsum  20458  chpub  20459  2sqlem8  20611  2sqlem9  20612  chebbnd1lem1  20618  chtppilimlem1  20622  rplogsumlem2  20634  rpvmasumlem  20636  rplogsum  20676  dirith2  20677  issubgo  20970  opidon  20989  chdmm1i  22056  chm0i  22069  ledii  22115  lejdii  22117  pjoml2i  22164  pjoml4i  22166  cmcmlem  22170  cmbr4i  22180  osumcori  22222  pjssmii  22260  mayete3i  22307  mayete3iOLD  22308  riesz4  22644  riesz1  22645  cnlnadjeu  22658  nmopadjlei  22668  pjclem1  22775  pjci  22780  mdbr3  22877  mdbr4  22878  dmdbr2  22883  dmdbr5  22888  ssmd2  22892  mdslj1i  22899  mdslj2i  22900  mdsl1i  22901  mdsl2bi  22903  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd2i  22910  csmdsymi  22914  cvexchlem  22948  atomli  22962  atcvat4i  22977  suppss2f  23201  off2  23208  partfun  23240  pnfneige0  23374  lmxrge0  23375  esumcst  23436  esumpcvgval  23446  hasheuni  23453  esumcvg  23454  sigainb  23497  indf1ofs  23609  probdif  23623  probmeasb  23633  cndprob01  23638  conpcon  23766  iccllyscon  23781  cvmsss2  23805  cvmcov2  23806  cvmopnlem  23809  cvmliftmolem2  23813  cvmlift2lem12  23845  nepss  24072  dedekindle  24083  elrn3  24120  dfon2lem4  24142  wfrlem4  24259  frrlem4  24284  domintrefb  25063  toplat  25290  reacomsmgrp1  25343  reacomsmgrp2  25344  reacomsmgrp3  25345  limptlimpr2lem2  25575  lvsovso  25626  tartarmap  25888  inttarcar  25901  cardtar  25904  bsstrs  26146  nbssntrs  26147  trer  26227  neiin  26250  neibastop1  26308  neibastop2lem  26309  topmeet  26313  filnetlem3  26329  heibor1lem  26533  heiborlem1  26535  heiborlem3  26537  heiborlem10  26544  elrfi  26769  elrfirn  26770  fnwe2lem2  27148  aomclem2  27152  lsmfgcl  27172  lmhmfgima  27182  lmhmfgsplit  27184  lmhmlnmsplit  27185  uvcff  27240  hbt  27334  mvdco  27388  acsfn1p  27507  onfrALTlem3  28309  onfrALTlem2  28311  onfrALTlem3VD  28663  onfrALTlem2VD  28665  bnj1293  28849  lshpinN  29179  lcvexchlem1  29224  lcvexchlem5  29228  pmod1i  30037  pmodN  30039  osumcllem7N  30151  pexmidlem4N  30162  dochdmj1  31580  dochexmidlem4  31653  lcfrlem25  31757  mapd1o  31838  mapdin  31852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator