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

Theorem inss2 3522
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 3493 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3521 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3339 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3279    C_ wss 3280
This theorem is referenced by:  difin0  3661  ordin  4571  onfr  4580  ordelinel  4639  relin2  4952  relres  5133  ssrnres  5268  cnvcnv  5282  fnresin2  5519  fresaunres2  5574  ssimaex  5747  exfo  5846  ffvresb  5859  ofrfval  6272  ofval  6273  ofrval  6274  offres  6278  off  6279  ofres  6280  ofco  6283  fnwelem  6420  fnse  6422  tpostpos  6458  smores3  6574  erinxp  6937  pmresg  7000  nnfi  7258  ixpfi2  7363  f1opwfi  7368  dffi2  7386  elfiun  7393  marypha1lem  7396  ordtypelem3  7445  ordtypelem6  7448  ordtypelem7  7449  hartogslem1  7467  unxpwdom  7513  epfrs  7623  tcmin  7636  bnd2  7773  tskwe  7793  r0weon  7850  infxpenlem  7851  fodomfi2  7897  infpwfien  7899  cdainf  8028  ackbij1lem6  8061  ackbij1lem9  8064  ackbij1lem10  8065  ackbij1lem11  8066  ackbij1lem15  8070  ackbij1lem16  8071  ackbij1lem18  8073  ackbij1b  8075  sdom2en01  8138  fin23lem26  8161  fin23lem13  8168  isfin1-3  8222  fin56  8229  fin1a2lem9  8244  ttukeylem6  8350  brdom3  8362  brdom5  8363  brdom4  8364  fpwwe2lem8  8468  fpwwe2lem9  8469  fpwwe2lem12  8472  fpwwe2  8474  canthwelem  8481  gruima  8633  ingru  8646  gruina  8649  grur1a  8650  ltrelpi  8722  ltrelnq  8759  nqerf  8763  fzfi  11266  rexanuz  12104  limsupgord  12221  limsupcl  12222  limsupgf  12224  limsupgle  12226  rlimres  12307  lo1res  12308  o1of2  12361  o1rlimmul  12367  ackbijnn  12562  bitsinv1  12909  bitsinvp1  12916  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  sadasslem  12937  sadeq  12939  smuval2  12949  smupval  12955  smueqlem  12957  prmrec  13245  isstruct2  13433  structcnvcnv  13435  ressbasss  13476  ressress  13481  restsspw  13614  pwsle  13669  submre  13785  isacs2  13833  isacs1i  13837  sscres  13978  rescabs  13988  resscat  14004  funcres2c  14053  coffth  14088  rescfth  14089  ressffth  14090  catccatid  14212  catcisolem  14216  catciso  14217  catcoppccl  14218  catcfuccl  14219  catcxpccl  14259  yoniso  14337  isdrs2  14351  isacs3lem  14547  acsinfd  14561  acsdomd  14562  psssdm2  14602  tsrss  14610  sylow2a  15208  lsmmod  15262  frgpnabllem2  15440  subrgpropd  15857  lssacs  15998  sralmod  16213  asplss  16343  ressmplbas  16474  subrgmpl  16478  opsrtoslem2  16500  mplind  16517  ressply1bas  16578  zlpirlem2  16724  zlpirlem3  16725  basdif0  16973  eltg4i  16980  ntrss2  17076  ntrin  17080  isopn3  17085  mreclatdemo  17115  neiptoptop  17150  restbas  17176  resttopon  17179  restuni2  17185  restcld  17190  restfpw  17197  neitr  17198  ordtrest  17220  subbascn  17272  cnrest2r  17305  cnpresti  17306  cnprest  17307  lmss  17316  cnrmi  17378  restcnrm  17380  resthauslem  17381  fincmp  17410  imacmp  17414  fiuncmp  17421  cmpfi  17425  cnconn  17438  iuncon  17444  clscon  17446  concompclo  17451  1stcrest  17469  subislly  17497  islly2  17500  cldllycmp  17511  hauspwdom  17517  kgeni  17522  llycmpkgen2  17535  1stckgenlem  17538  ptbasfi  17566  txcls  17589  ptclsg  17600  txcnp  17605  ptcnplem  17606  txtube  17625  txcmplem1  17626  txcmplem2  17627  txkgen  17637  xkopt  17640  xkococnlem  17644  txcon  17674  basqtop  17696  tgqtop  17697  kqdisj  17717  kqnrmlem1  17728  kqnrmlem2  17729  nrmhmph  17779  infil  17848  fbasrn  17869  trfg  17876  uzrest  17882  isufil2  17893  fmfnfmlem4  17942  hauspwpwf1  17972  txflf  17991  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem2  18037  tmdgsum2  18079  tsmsres  18126  tsmsxplem1  18135  ustexsym  18198  ustund  18204  trust  18212  utoptop  18217  restutop  18220  blres  18414  met2ndci  18505  metrest  18507  restmetu  18570  tgioo  18780  zdis  18800  reconnlem2  18811  reconn  18812  cnheibor  18933  lebnum  18942  nmoleub2lem3  19076  nmoleub3  19080  cphsqrcl  19100  tchcph  19147  cfilresi  19201  cfilres  19202  caussi  19203  causs  19204  minveclem4b  19285  minveclem4  19286  ovolfcl  19316  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovolfsval  19320  ovolfsf  19321  ovollb  19328  ovoliunlem1  19351  ovolicc2lem1  19366  ovolicc2lem2  19367  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  ovolicc2  19371  nulmbl  19383  voliunlem1  19397  ioombl1lem4  19408  ovolfs2  19416  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2a  19427  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombllem6  19433  uniioombl  19434  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  volcn  19451  volivth  19452  vitalilem2  19454  vitalilem4  19456  mbfadd  19506  mbfsub  19507  i1fima  19523  i1fima2  19524  i1fd  19526  i1fadd  19540  i1fmul  19541  itg1addlem2  19542  itg1addlem4  19544  itg1addlem5  19545  i1fres  19550  mbfmul  19571  itg2cnlem2  19607  bddmulibl  19683  ellimc2  19717  ellimc3  19719  limcflf  19721  limcresi  19725  limciun  19734  dvreslem  19749  dvres2lem  19750  dvres3a  19754  cpnres  19776  dvaddbr  19777  dvmulbr  19778  dvmptres3  19795  lhop1lem  19850  pf1rcl  19922  ig1peu  20047  taylfvallem1  20226  tayl0  20231  rlimcnp2  20758  xrlimcnp  20760  ppisval  20839  chtf  20844  efchtcl  20847  chtge0  20848  ppinprm  20888  chtprm  20889  chtnprm  20890  chtwordi  20892  chtdif  20894  efchtdvds  20895  chtlepsi  20943  chtleppi  20947  pclogsum  20952  chpval2  20955  chpchtsum  20956  chpub  20957  2sqlem8  21109  2sqlem9  21110  chebbnd1lem1  21116  chtppilimlem1  21120  rplogsumlem2  21132  rpvmasumlem  21134  rplogsum  21174  dirith2  21175  issubgo  21844  opidon  21863  chdmm1i  22932  chm0i  22945  ledii  22991  lejdii  22993  pjoml2i  23040  pjoml4i  23042  cmcmlem  23046  cmbr4i  23056  osumcori  23098  pjssmii  23136  mayete3i  23183  mayete3iOLD  23184  riesz4  23520  riesz1  23521  cnlnadjeu  23534  nmopadjlei  23544  pjclem1  23651  pjci  23656  mdbr3  23753  mdbr4  23754  dmdbr2  23759  dmdbr5  23764  ssmd2  23768  mdslj1i  23775  mdslj2i  23776  mdsl1i  23777  mdsl2bi  23779  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd2i  23786  csmdsymi  23790  cvexchlem  23824  atomli  23838  atcvat4i  23853  disjxpin  23981  imadifxp  23991  suppss2f  24002  off2  24007  partfun  24040  resspos  24140  resstos  24141  subofld  24198  pnfneige0  24289  lmxrge0  24290  qqhnm  24327  qqhcn  24328  rrhre  24340  indf1ofs  24376  gsumesum  24404  esumlub  24405  esumcst  24408  esumpcvgval  24421  hasheuni  24428  esumcvg  24429  sigainb  24472  measunl  24523  sibfof  24607  probdif  24631  probmeasb  24641  cndprob01  24646  conpcon  24875  iccllyscon  24890  cvmsss2  24914  cvmcov2  24915  cvmopnlem  24918  cvmliftmolem2  24922  cvmlift2lem12  24954  nepss  25128  dedekindle  25141  elrn3  25334  dfon2lem4  25356  wfrlem4  25473  frrlem4  25498  mblfinlem3  26145  mbfposadd  26153  trer  26209  neiin  26225  neibastop1  26278  neibastop2lem  26279  topmeet  26283  filnetlem3  26299  heibor1lem  26408  heiborlem1  26410  heiborlem3  26412  heiborlem10  26419  elrfi  26638  elrfirn  26639  fnwe2lem2  27016  aomclem2  27020  lsmfgcl  27040  lmhmfgima  27050  lmhmfgsplit  27052  lmhmlnmsplit  27053  uvcff  27108  hbt  27202  mvdco  27256  acsfn1p  27375  onfrALTlem3  28341  onfrALTlem2  28343  onfrALTlem3VD  28708  onfrALTlem2VD  28710  bnj1293  28894  lshpinN  29472  lcvexchlem1  29517  lcvexchlem5  29521  pmod1i  30330  pmodN  30332  osumcllem7N  30444  pexmidlem4N  30455  dochdmj1  31873  dochexmidlem4  31946  lcfrlem25  32050  mapd1o  32131  mapdin  32145
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator