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

Theorem inss2 3392
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 3363 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3391 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3211 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3153    C_ wss 3154
This theorem is referenced by:  difin0  3529  ordin  4422  onfr  4431  ordelinel  4491  relin2  4804  relres  4983  ssrnres  5116  cnvcnv  5126  fnresin2  5325  fresaunres2  5379  ssimaex  5546  exfo  5640  ffvresb  5652  ofrfval  6048  ofval  6049  ofrval  6050  offres  6054  off  6055  ofres  6056  ofco  6059  fnwelem  6192  fnse  6194  tpostpos  6216  smores3  6366  erinxp  6729  pmresg  6791  nnfi  7049  ixpfi2  7150  f1opwfi  7155  dffi2  7172  elfiun  7179  marypha1lem  7182  ordtypelem3  7231  ordtypelem6  7234  ordtypelem7  7235  hartogslem1  7253  unxpwdom  7299  epfrs  7409  tcmin  7422  bnd2  7559  tskwe  7579  r0weon  7636  infxpenlem  7637  fodomfi2  7683  infpwfien  7685  cdainf  7814  ackbij1lem6  7847  ackbij1lem9  7850  ackbij1lem10  7851  ackbij1lem11  7852  ackbij1lem15  7856  ackbij1lem16  7857  ackbij1lem18  7859  ackbij1b  7861  sdom2en01  7924  fin23lem26  7947  fin23lem13  7954  isfin1-3  8008  fin56  8015  fin1a2lem9  8030  ttukeylem6  8137  brdom3  8149  brdom5  8150  brdom4  8151  fpwwe2lem8  8255  fpwwe2lem9  8256  fpwwe2lem12  8259  fpwwe2  8261  canthwelem  8268  gruima  8420  ingru  8433  gruina  8436  grur1a  8437  ltrelpi  8509  ltrelnq  8546  nqerf  8550  fzfi  11029  rexanuz  11824  limsupgord  11941  limsupcl  11942  limsupgf  11944  limsupgle  11946  rlimres  12027  lo1res  12028  o1of2  12081  o1rlimmul  12087  ackbijnn  12281  bitsinv1  12628  bitsinvp1  12635  sadcaddlem  12643  sadadd2lem  12645  sadadd3  12647  sadaddlem  12652  sadasslem  12656  sadeq  12658  smuval2  12668  smupval  12674  smueqlem  12676  prmrec  12964  isstruct2  13152  structcnvcnv  13154  ressbasss  13195  ressress  13200  restsspw  13331  pwsle  13386  submre  13502  isacs2  13550  isacs1i  13554  sscres  13695  rescabs  13705  resscat  13721  funcres2c  13770  coffth  13805  rescfth  13806  ressffth  13807  catccatid  13929  catcisolem  13933  catciso  13934  catcoppccl  13935  catcfuccl  13936  catcxpccl  13976  yoniso  14054  isdrs2  14068  isacs3lem  14264  acsinfd  14278  acsdomd  14279  psssdm2  14319  tsrss  14327  sylow2a  14925  lsmmod  14979  frgpnabllem2  15157  subrgpropd  15574  lssacs  15719  sralmod  15934  asplss  16064  ressmplbas  16195  subrgmpl  16199  opsrtoslem2  16221  mplind  16238  ressply1bas  16302  zlpirlem2  16437  zlpirlem3  16438  basdif0  16686  eltg4i  16693  ntrss2  16789  ntrin  16793  isopn3  16798  mreclatdemo  16828  restbas  16884  resttopon  16887  restuni2  16893  restcld  16898  restfpw  16905  ordtrest  16927  subbascn  16979  cnrest2r  17010  cnpresti  17011  cnprest  17012  lmss  17021  cnrmi  17083  restcnrm  17085  resthauslem  17086  fincmp  17115  imacmp  17119  fiuncmp  17126  cmpfi  17130  cnconn  17143  iuncon  17149  clscon  17151  concompclo  17156  1stcrest  17174  subislly  17202  islly2  17205  cldllycmp  17216  hauspwdom  17222  kgeni  17227  llycmpkgen2  17240  1stckgenlem  17243  ptbasfi  17271  txcls  17294  ptclsg  17304  txcnp  17309  ptcnplem  17310  txtube  17329  txcmplem1  17330  txcmplem2  17331  txkgen  17341  xkopt  17344  xkococnlem  17348  txcon  17378  basqtop  17397  tgqtop  17398  kqdisj  17418  kqnrmlem1  17429  kqnrmlem2  17430  nrmhmph  17480  infil  17553  fbasrn  17574  trfg  17581  uzrest  17587  isufil2  17598  fmfnfmlem4  17647  hauspwpwf1  17677  txflf  17696  alexsubALTlem3  17738  alexsubALTlem4  17739  ptcmplem2  17742  tmdgsum2  17774  tsmsres  17821  tsmsxplem1  17830  blres  17972  met2ndci  18063  metrest  18065  tgioo  18297  zdis  18317  reconnlem2  18327  reconn  18328  cnheibor  18448  lebnum  18457  nmoleub2lem3  18591  nmoleub3  18595  cphsqrcl  18615  tchcph  18662  cfilresi  18716  cfilres  18717  caussi  18718  causs  18719  minveclem4b  18790  minveclem4  18791  ovolfcl  18821  ovolfioo  18822  ovolficc  18823  ovolficcss  18824  ovolfsval  18825  ovolfsf  18826  ovollb  18833  ovoliunlem1  18856  ovolicc2lem1  18871  ovolicc2lem2  18872  ovolicc2lem3  18873  ovolicc2lem4  18874  ovolicc2lem5  18875  ovolicc2  18876  nulmbl  18888  voliunlem1  18902  ioombl1lem4  18913  ovolfs2  18921  uniiccdif  18928  uniioovol  18929  uniiccvol  18930  uniioombllem2a  18932  uniioombllem2  18933  uniioombllem3a  18934  uniioombllem3  18935  uniioombllem4  18936  uniioombllem5  18937  uniioombllem6  18938  uniioombl  18939  dyadmbllem  18949  dyadmbl  18950  opnmbllem  18951  volcn  18956  volivth  18957  vitalilem2  18959  vitalilem4  18961  mbfadd  19011  mbfsub  19012  i1fima  19028  i1fima2  19029  i1fd  19031  i1fadd  19045  i1fmul  19046  itg1addlem2  19047  itg1addlem4  19049  itg1addlem5  19050  i1fres  19055  mbfmul  19076  itg2cnlem2  19112  bddmulibl  19188  ellimc2  19222  ellimc3  19224  limcflf  19226  limcresi  19230  limciun  19239  dvreslem  19254  dvres2lem  19255  dvres3a  19259  cpnres  19281  dvaddbr  19282  dvmulbr  19283  dvmptres3  19300  lhop1lem  19355  pf1rcl  19427  ig1peu  19552  taylfvallem1  19731  tayl0  19736  rlimcnp2  20256  xrlimcnp  20258  ppisval  20336  chtf  20341  efchtcl  20344  chtge0  20345  ppinprm  20385  chtprm  20386  chtnprm  20387  chtwordi  20389  chtdif  20391  efchtdvds  20392  chtlepsi  20440  chtleppi  20444  pclogsum  20449  chpval2  20452  chpchtsum  20453  chpub  20454  2sqlem8  20606  2sqlem9  20607  chebbnd1lem1  20613  chtppilimlem1  20617  rplogsumlem2  20629  rpvmasumlem  20631  rplogsum  20671  dirith2  20672  issubgo  20963  opidon  20982  chdmm1i  22049  chm0i  22062  ledii  22108  lejdii  22110  pjoml2i  22157  pjoml4i  22159  cmcmlem  22163  cmbr4i  22173  osumcori  22215  pjssmii  22253  mayete3i  22300  mayete3iOLD  22301  riesz4  22637  riesz1  22638  cnlnadjeu  22651  nmopadjlei  22661  pjclem1  22768  pjci  22773  mdbr3  22870  mdbr4  22871  dmdbr2  22876  dmdbr5  22881  ssmd2  22885  mdslj1i  22892  mdslj2i  22893  mdsl1i  22894  mdsl2bi  22896  mdslmd1lem1  22898  mdslmd1lem2  22899  mdslmd2i  22903  csmdsymi  22907  cvexchlem  22941  atomli  22955  atcvat4i  22970  conpcon  23171  iccllyscon  23186  cvmsss2  23210  cvmcov2  23211  cvmopnlem  23214  cvmliftmolem2  23218  cvmlift2lem12  23250  nepss  23477  dedekindle  23487  dfon2lem4  23544  wfrlem4  23661  frrlem4  23686  domintrefb  24462  toplat  24690  reacomsmgrp1  24743  reacomsmgrp2  24744  reacomsmgrp3  24745  limptlimpr2lem2  24975  lvsovso  25026  tartarmap  25288  inttarcar  25301  cardtar  25304  bsstrs  25546  nbssntrs  25547  trer  25627  neiin  25650  neibastop1  25708  neibastop2lem  25709  topmeet  25713  filnetlem3  25729  heibor1lem  25933  heiborlem1  25935  heiborlem3  25937  heiborlem10  25944  elrfi  26169  elrfirn  26170  fnwe2lem2  26548  aomclem2  26552  lsmfgcl  26572  lmhmfgima  26582  lmhmfgsplit  26584  lmhmlnmsplit  26585  uvcff  26640  hbt  26734  mvdco  26788  acsfn1p  26907  onfrALTlem3  27581  onfrALTlem2  27583  onfrALTlem3VD  27932  onfrALTlem2VD  27934  bnj1293  28117  lshpinN  28447  lcvexchlem1  28492  lcvexchlem5  28496  pmod1i  29305  pmodN  29307  osumcllem7N  29419  pexmidlem4N  29430  dochdmj1  30848  dochexmidlem4  30921  lcfrlem25  31025  mapd1o  31106  mapdin  31120
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator