Theorem inss2 4197

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 4168	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4196	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3991	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3910   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  inindif  4334  difin0  4433  iunxdif3  5054  relin2  5767  relres  5965  idssxp  6009  ssrnres  6139  cnvrescnv  6156  ordin  6350  onfr  6359  ordelinel  6423  fnresin2  6626  fresaunres2  6714  ssimaex  6928  exfo  7059  ffvresb  7079  fnfvimad  7190  ofrfvalg  7641  ofval  7644  ofrval  7645  off  7651  ofres  7652  ofco  7658  fnwelem  8087  fnse  8089  fprlem1  8256  tfrlem5  8325  pmresg  8820  ixpfi2  9277  elfiun  9357  marypha1lem  9360  ordtypelem6  9452  ordtypelem7  9453  hartogslem1  9471  unxpwdom  9518  epfrs  9660  tcmin  9670  bnd2  9822  tskwe  9879  r0weon  9941  infxpenlem  9942  djuinf  10118  ackbij1lem9  10156  ackbij1lem10  10157  ackbij1lem15  10162  ackbij1lem16  10163  ackbij1b  10167  sdom2en01  10231  fin23lem26  10254  fin23lem13  10261  isfin1-3  10315  fin56  10322  fin1a2lem9  10337  brdom3  10457  brdom5  10458  brdom4  10459  fpwwe2lem11  10570  fpwwe2  10572  canthwelem  10579  gruima  10731  ingru  10744  gruina  10747  grur1a  10748  ltrelpi  10818  ltrelnq  10855  nqerf  10859  fzfi  13913  xptrrel  14922  rexanuz  15288  limsupgord  15414  limsupcl  15415  limsupgf  15417  limsupgle  15419  o1of2  15555  o1rlimmul  15561  ackbijnn  15770  bitsinv1  16388  bitsinvp1  16395  sadcaddlem  16403  sadadd2lem  16405  sadadd3  16407  sadaddlem  16412  sadasslem  16416  sadeq  16418  smupval  16434  prmrec  16869  structcnvcnv  17099  ressbasss  17185  ressbasssOLD  17186  ressress  17193  restsspw  17370  submre  17542  isacs1i  17594  rescabs  17771  resscat  17790  funcres2c  17841  ressffth  17878  catccatid  18044  catcisolem  18048  catciso  18049  yoniso  18222  acsinfd  18491  acsdomd  18492  tsrss  18524  idresefmnd  18802  idrespermg  19317  mvdco  19351  lsmmod  19581  rnghmresfn  20504  rnghmsscmap  20515  rhmresfn  20533  rhmsscmap  20544  rhmsubclem4  20573  acsfn1p  20684  lssacs  20849  lidlssbas  21099  zringlpirlem2  21349  zringlpirlem3  21350  asplss  21759  ressmplbas  21911  subrgmpl  21915  mplind  21953  ressply1bas  22089  pf1rcl  22212  ressply1evl  22233  evls1addd  22234  evls1muld  22235  evls1vsca  22236  evls1maprhm  22239  ofco2  22314  basdif0  22816  eltg4i  22823  ntrss2  22920  ntrin  22924  isopn3  22929  resttopon  23024  restuni2  23030  restcld  23035  restfpw  23042  neitr  23043  cnrest2r  23150  cnpresti  23151  cnprest  23152  lmss  23161  cnrmi  23223  restcnrm  23225  resthauslem  23226  imacmp  23260  fiuncmp  23267  subislly  23344  islly2  23347  cldllycmp  23358  hauspwdom  23364  kgeni  23400  llycmpkgen2  23413  ptbasfi  23444  ptclsg  23478  ptcnplem  23484  txtube  23503  txcmplem2  23505  txkgen  23515  kqdisj  23595  fbasrn  23747  trfg  23754  isufil2  23771  fmfnfmlem4  23820  hauspwpwf1  23850  txflf  23869  alexsubALTlem4  23913  tmdgsum2  23959  tsmsres  24007  tsmsxplem1  24016  ustexsym  24079  ustund  24085  trust  24093  utoptop  24098  restutop  24101  metrest  24388  restmetu  24434  tgioo  24660  reconnlem2  24692  cphsqrtcl  25060  tcphcph  25113  cfilresi  25171  caussi  25173  causs  25174  ovolfioo  25344  ovolficc  25345  ovolficcss  25346  ovolfsf  25348  ovollb  25356  ovolicc2lem1  25394  ovolicc2lem2  25395  ovolicc2lem3  25396  ovolicc2lem4  25397  ovolicc2  25399  nulmbl  25412  voliunlem1  25427  ovolfs2  25448  uniiccdif  25455  uniioovol  25456  uniiccvol  25457  uniioombllem2  25460  uniioombllem3a  25461  uniioombllem3  25462  uniioombllem4  25463  uniioombllem5  25464  uniioombllem6  25465  uniioombl  25466  dyadmbllem  25476  dyadmbl  25477  opnmbllem  25478  volcn  25483  volivth  25484  mbfadd  25538  mbfsub  25539  i1fima  25555  i1fima2  25556  i1fd  25558  i1fadd  25572  i1fmul  25573  itg1addlem2  25574  itg1addlem4  25576  itg1addlem5  25577  i1fres  25582  mbfmul  25603  bddmulibl  25716  ellimc2  25754  ellimc3  25756  limcflf  25758  limcresi  25762  limciun  25771  dvreslem  25786  dvres2lem  25787  dvres3a  25791  cpnres  25815  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  dvmptres3  25836  lhop1lem  25894  rlimcnp2  26852  xrlimcnp  26854  chpchtsum  27106  2sqlem8  27313  2sqlem9  27314  rpvmasumlem  27374  rplogsum  27414  dirith2  27415  nosupbnd2  27604  axtgsegcon  28367  axtg5seg  28368  axtgbtwnid  28369  axtgpasch  28370  axtgcont1  28371  tglng  28449  chdmm1i  31379  chm0i  31392  ledii  31438  lejdii  31440  pjoml2i  31487  pjoml4i  31489  cmcmlem  31493  cmbr4i  31503  osumcori  31545  pjssmii  31583  mayete3i  31630  riesz4  31966  riesz1  31967  cnlnadjeu  31980  nmopadjlei  31990  pjclem1  32097  pjci  32102  mdbr3  32199  mdbr4  32200  dmdbr2  32205  dmdbr5  32210  ssmd2  32214  mdslj1i  32221  mdslj2i  32222  mdsl1i  32223  mdsl2bi  32225  mdslmd1lem1  32227  mdslmd1lem2  32228  mdslmd2i  32232  csmdsymi  32236  cvexchlem  32270  atomli  32284  atcvat4i  32299  difininv  32419  disjxpin  32490  imadifxp  32503  off2  32538  mptiffisupp  32589  indsumin  32758  indf1ofs  32762  resspos  32865  resstos  32866  submomnd  32997  suborng  33266  idlinsubrg  33375  ressply1invg  33511  evls1subd  33514  algextdeglem7  33686  algextdeglem8  33687  ordtrestNEW  33884  pnfneige0  33914  lmxrge0  33915  qqhnm  33953  qqhcn  33954  rrhre  33984  gsumesum  34022  esumlub  34023  esumcst  34026  esumpcvgval  34041  hasheuni  34048  esumcvg  34049  sigainb  34099  carsgclctunlem2  34283  sibfinima  34303  sibfof  34304  eulerpartlemelr  34321  eulerpartlemgh  34342  eulerpartlemgf  34343  eulerpartlemgs2  34344  eulerpartlemn  34345  probmeasb  34394  cndprob01  34399  hashreprin  34584  reprfi2  34587  breprexpnat  34598  hgt750lemd  34612  hgt750lema  34621  tgoldbachgtde  34624  tgoldbachgtda  34625  tgoldbachgt  34627  bnj1293  34779  connpconn  35195  iccllysconn  35210  cvmsss2  35234  cvmcov2  35235  cvmopnlem  35238  cvmliftmolem2  35242  cvmlift2lem12  35274  mvrsfpw  35466  elmsta  35508  msubvrs  35520  mclsind  35530  nepss  35678  dfon2lem4  35747  trer  36277  neiin  36293  neibastop1  36320  neibastop2lem  36321  topmeet  36325  filnetlem3  36341  weiunfr  36428  bj-disj2r  36989  bj-restpw  37053  bj-restb  37055  bj-restuni2  37059  bj-ablsscmn  37239  topdifinffinlem  37308  opnmbllem0  37623  mblfinlem4  37627  mbfposadd  37634  heibor1lem  37776  heiborlem1  37778  heiborlem3  37780  heiborlem10  37787  opidonOLD  37819  disjimin  38716  lshpinN  38955  lcvexchlem1  39000  lcvexchlem5  39004  pmod1i  39815  pmodN  39817  osumcllem7N  39929  pexmidlem4N  39940  dochdmj1  41357  dochexmidlem4  41430  lcfrlem25  41534  mapd1o  41615  mapdin  41629  elrfi  42655  elrfirn  42656  fnwe2lem2  43013  aomclem2  43017  lsmfgcl  43036  lmhmfgima  43046  lmhmfgsplit  43048  lmhmlnmsplit  43049  hbt  43092  ofoafg  43316  trrelind  43627  iunrelexp0  43664  isotone2  44011  grumnudlem  44247  ismnushort  44263  onfrALTlem3  44507  onfrALTlem2  44509  onfrALTlem3VD  44849  onfrALTlem2VD  44851  iunconnlem2  44897  wfac8prim  44965  restuni6  45089  disjinfi  45159  inmap  45176  fsumiunss  45546  islptre  45590  sumnnodd  45601  limcresiooub  45613  limcresioolb  45614  limcleqr  45615  limclner  45622  limclr  45626  limsuplesup  45670  limsuppnfdlem  45672  limsupres  45676  liminfgord  45725  liminfgf  45729  liminfcl  45734  limsupresxr  45737  liminfresxr  45738  liminfval2  45739  liminflelimsuplem  45746  liminfvalxr  45754  icccncfext  45858  fourierdlem20  46098  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem76  46153  fourierdlem103  46180  fourierdlem104  46181  fourierdlem113  46190  fouriersw  46202  salgencntex  46314  sge0less  46363  sge0resplit  46377  sge0split  46380  sge0iunmptlemre  46386  sge0fodjrnlem  46387  caragencmpl  46506  ovolval2lem  46614  ovolval2  46615  ovolval3  46618  ovolval4lem2  46621  sssmf  46709  fcoreslem4  47040  fcoresf1  47043  fcoresfo  47045  3f1oss1  47049  rngchomrnghmresALTV  48240  termc  49481