Theorem inss2 4160

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	⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Proof of Theorem inss2

Step	Hyp	Ref	Expression
1		incom 4131	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4159	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3952	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  difin0  4404  iunxdif3  5020  relin2  5712  relres  5909  idssxp  5945  ssrnres  6070  cnvrescnv  6087  ordin  6281  onfr  6290  ordelinel  6349  fnresin2  6542  fresaunres2  6630  ssimaex  6835  exfo  6963  ffvresb  6980  fnfvimad  7092  ofrfvalg  7519  ofval  7522  ofrval  7523  off  7529  ofres  7530  ofco  7534  fnwelem  7943  fnse  7945  fprlem1  8087  tfrlem5  8182  pmresg  8616  nnfiOLD  8946  ixpfi2  9047  elfiun  9119  marypha1lem  9122  ordtypelem6  9212  ordtypelem7  9213  hartogslem1  9231  unxpwdom  9278  epfrs  9420  tcmin  9430  bnd2  9582  tskwe  9639  r0weon  9699  infxpenlem  9700  djuinf  9875  ackbij1lem9  9915  ackbij1lem10  9916  ackbij1lem15  9921  ackbij1lem16  9922  ackbij1b  9926  sdom2en01  9989  fin23lem26  10012  fin23lem13  10019  isfin1-3  10073  fin56  10080  fin1a2lem9  10095  brdom3  10215  brdom5  10216  brdom4  10217  fpwwe2lem11  10328  fpwwe2  10330  canthwelem  10337  gruima  10489  ingru  10502  gruina  10505  grur1a  10506  ltrelpi  10576  ltrelnq  10613  nqerf  10617  fzfi  13620  xptrrel  14619  rexanuz  14985  limsupgord  15109  limsupcl  15110  limsupgf  15112  limsupgle  15114  o1of2  15250  o1rlimmul  15256  ackbijnn  15468  bitsinv1  16077  bitsinvp1  16084  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  sadasslem  16105  sadeq  16107  smupval  16123  prmrec  16551  structcnvcnv  16782  ressbasss  16876  ressress  16884  restsspw  17059  submre  17231  isacs1i  17283  rescabs  17464  resscat  17483  funcres2c  17533  ressffth  17570  catccatid  17737  catcisolem  17741  catciso  17742  yoniso  17919  acsinfd  18189  acsdomd  18190  tsrss  18222  idresefmnd  18453  idrespermg  18934  mvdco  18968  lsmmod  19196  acsfn1p  19982  lssacs  20144  zringlpirlem2  20597  zringlpirlem3  20598  asplss  20988  ressmplbas  21139  subrgmpl  21143  mplind  21188  ressply1bas  21310  pf1rcl  21425  ofco2  21508  basdif0  22011  eltg4i  22018  ntrss2  22116  ntrin  22120  isopn3  22125  resttopon  22220  restuni2  22226  restcld  22231  restfpw  22238  neitr  22239  cnrest2r  22346  cnpresti  22347  cnprest  22348  lmss  22357  cnrmi  22419  restcnrm  22421  resthauslem  22422  imacmp  22456  fiuncmp  22463  subislly  22540  islly2  22543  cldllycmp  22554  hauspwdom  22560  kgeni  22596  llycmpkgen2  22609  ptbasfi  22640  ptclsg  22674  ptcnplem  22680  txtube  22699  txcmplem2  22701  txkgen  22711  kqdisj  22791  fbasrn  22943  trfg  22950  isufil2  22967  fmfnfmlem4  23016  hauspwpwf1  23046  txflf  23065  alexsubALTlem4  23109  tmdgsum2  23155  tsmsres  23203  tsmsxplem1  23212  ustexsym  23275  ustund  23281  trust  23289  utoptop  23294  restutop  23297  metrest  23586  restmetu  23632  tgioo  23865  reconnlem2  23896  cphsqrtcl  24253  tcphcph  24306  cfilresi  24364  caussi  24366  causs  24367  ovolfioo  24536  ovolficc  24537  ovolficcss  24538  ovolfsf  24540  ovollb  24548  ovolicc2lem1  24586  ovolicc2lem2  24587  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2  24591  nulmbl  24604  voliunlem1  24619  ovolfs2  24640  uniiccdif  24647  uniioovol  24648  uniiccvol  24649  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombllem6  24657  uniioombl  24658  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  volcn  24675  volivth  24676  mbfadd  24730  mbfsub  24731  i1fima  24747  i1fima2  24748  i1fd  24750  i1fadd  24764  i1fmul  24765  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  i1fres  24775  mbfmul  24796  bddmulibl  24908  ellimc2  24946  ellimc3  24948  limcflf  24950  limcresi  24954  limciun  24963  dvreslem  24978  dvres2lem  24979  dvres3a  24983  cpnres  25006  dvaddbr  25007  dvmulbr  25008  dvmptres3  25025  lhop1lem  25082  rlimcnp2  26021  xrlimcnp  26023  chpchtsum  26272  2sqlem8  26479  2sqlem9  26480  rpvmasumlem  26540  rplogsum  26580  dirith2  26581  axtgsegcon  26729  axtg5seg  26730  axtgbtwnid  26731  axtgpasch  26732  axtgcont1  26733  tglng  26811  chdmm1i  29740  chm0i  29753  ledii  29799  lejdii  29801  pjoml2i  29848  pjoml4i  29850  cmcmlem  29854  cmbr4i  29864  osumcori  29906  pjssmii  29944  mayete3i  29991  riesz4  30327  riesz1  30328  cnlnadjeu  30341  nmopadjlei  30351  pjclem1  30458  pjci  30463  mdbr3  30560  mdbr4  30561  dmdbr2  30566  dmdbr5  30571  ssmd2  30575  mdslj1i  30582  mdslj2i  30583  mdsl1i  30584  mdsl2bi  30586  mdslmd1lem1  30588  mdslmd1lem2  30589  mdslmd2i  30593  csmdsymi  30597  cvexchlem  30631  atomli  30645  atcvat4i  30660  inindif  30764  difininv  30765  disjxpin  30828  imadifxp  30841  off2  30879  resspos  31146  resstos  31147  submomnd  31238  suborng  31416  idlinsubrg  31510  ordtrestNEW  31773  pnfneige0  31803  lmxrge0  31804  qqhnm  31840  qqhcn  31841  rrhre  31871  indsumin  31890  indf1ofs  31894  gsumesum  31927  esumlub  31928  esumcst  31931  esumpcvgval  31946  hasheuni  31953  esumcvg  31954  sigainb  32004  carsgclctunlem2  32186  sibfinima  32206  sibfof  32207  eulerpartlemelr  32224  eulerpartlemgh  32245  eulerpartlemgf  32246  eulerpartlemgs2  32247  eulerpartlemn  32248  probmeasb  32297  cndprob01  32302  hashreprin  32500  reprfi2  32503  breprexpnat  32514  hgt750lemd  32528  hgt750lema  32537  tgoldbachgtde  32540  tgoldbachgtda  32541  tgoldbachgt  32543  bnj1293  32696  connpconn  33097  iccllysconn  33112  cvmsss2  33136  cvmcov2  33137  cvmopnlem  33140  cvmliftmolem2  33144  cvmlift2lem12  33176  mvrsfpw  33368  elmsta  33410  msubvrs  33422  mclsind  33432  nepss  33564  dfon2lem4  33668  nosupbnd2  33846  trer  34432  neiin  34448  neibastop1  34475  neibastop2lem  34476  topmeet  34480  filnetlem3  34496  bj-disj2r  35145  bj-restpw  35190  bj-restb  35192  bj-restuni2  35196  bj-ablsscmn  35376  topdifinffinlem  35445  opnmbllem0  35740  mblfinlem4  35744  mbfposadd  35751  heibor1lem  35894  heiborlem1  35896  heiborlem3  35898  heiborlem10  35905  opidonOLD  35937  disjimin  36786  lshpinN  36930  lcvexchlem1  36975  lcvexchlem5  36979  pmod1i  37789  pmodN  37791  osumcllem7N  37903  pexmidlem4N  37914  dochdmj1  39331  dochexmidlem4  39404  lcfrlem25  39508  mapd1o  39589  mapdin  39603  elrfi  40432  elrfirn  40433  fnwe2lem2  40792  aomclem2  40796  lsmfgcl  40815  lmhmfgima  40825  lmhmfgsplit  40827  lmhmlnmsplit  40828  hbt  40871  trrelind  41162  iunrelexp0  41199  isotone2  41548  grumnudlem  41792  ismnushort  41808  onfrALTlem3  42053  onfrALTlem2  42055  onfrALTlem3VD  42396  onfrALTlem2VD  42398  iunconnlem2  42444  restuni6  42560  disjinfi  42620  inmap  42638  dmresss  42663  fsumiunss  43006  islptre  43050  sumnnodd  43061  limcresiooub  43073  limcresioolb  43074  limcleqr  43075  limclner  43082  limclr  43086  limsuplesup  43130  limsuppnfdlem  43132  limsupres  43136  liminfgord  43185  liminfgf  43189  liminfcl  43194  limsupresxr  43197  liminfresxr  43198  liminfval2  43199  liminflelimsuplem  43206  liminfvalxr  43214  icccncfext  43318  fourierdlem20  43558  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem76  43613  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  fouriersw  43662  salgencntex  43772  sge0less  43820  sge0resplit  43834  sge0split  43837  sge0iunmptlemre  43843  sge0fodjrnlem  43844  caragencmpl  43963  ovolval2lem  44071  ovolval2  44072  ovolval3  44075  ovolval4lem2  44078  sssmf  44161  fcoreslem4  44447  fcoresf1  44450  fcoresfo  44452  lidlssbas  45368  rnghmresfn  45409  rnghmsscmap  45420  rngchomrnghmresALTV  45442  rhmresfn  45455  rhmsscmap  45466  rhmsubclem4  45535