Theorem inss2 4178

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 4149	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4177	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3969	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3888   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  inindif  4315  difin0  4414  iunxdif3  5037  relin2  5769  relres  5970  idssxp  6014  ssrnres  6142  cnvrescnv  6159  ordin  6353  onfr  6362  ordelinel  6426  fnresin2  6624  fresaunres2  6712  ssimaex  6925  exfo  7057  ffvresb  7078  fnfvimad  7189  ofrfvalg  7639  ofval  7642  ofrval  7643  off  7649  ofres  7650  ofco  7656  fnwelem  8081  fnse  8083  fprlem1  8250  tfrlem5  8319  pmresg  8818  ixpfi2  9260  elfiun  9343  marypha1lem  9346  ordtypelem6  9438  ordtypelem7  9439  hartogslem1  9457  unxpwdom  9504  epfrs  9652  tcmin  9660  bnd2  9817  tskwe  9874  r0weon  9934  infxpenlem  9935  djuinf  10111  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem15  10155  ackbij1lem16  10156  ackbij1b  10160  sdom2en01  10224  fin23lem26  10247  fin23lem13  10254  isfin1-3  10308  fin56  10315  fin1a2lem9  10330  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem11  10564  fpwwe2  10566  canthwelem  10573  gruima  10725  ingru  10738  gruina  10741  grur1a  10742  ltrelpi  10812  ltrelnq  10849  nqerf  10853  fzfi  13934  xptrrel  14942  rexanuz  15308  limsupgord  15434  limsupcl  15435  limsupgf  15437  limsupgle  15439  o1of2  15575  o1rlimmul  15581  ackbijnn  15793  bitsinv1  16411  bitsinvp1  16418  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  sadeq  16441  smupval  16457  prmrec  16893  structcnvcnv  17123  ressbasss  17209  ressbasssOLD  17210  ressress  17217  restsspw  17394  submre  17567  isacs1i  17623  rescabs  17800  resscat  17819  funcres2c  17870  ressffth  17907  catccatid  18073  catcisolem  18077  catciso  18078  yoniso  18251  resspos  18395  resstos  18396  acsinfd  18522  acsdomd  18523  tsrss  18555  idresefmnd  18867  idrespermg  19386  mvdco  19420  lsmmod  19650  submomnd  20107  rnghmresfn  20596  rnghmsscmap  20607  rhmresfn  20625  rhmsscmap  20636  rhmsubclem4  20665  acsfn1p  20776  suborng  20853  lssacs  20962  lidlssbas  21211  zringlpirlem2  21443  zringlpirlem3  21444  asplss  21853  ressmplbas  22006  subrgmpl  22010  mplind  22048  ressply1bas  22192  pf1rcl  22314  ressply1evl  22335  evls1addd  22336  evls1muld  22337  evls1vsca  22338  evls1maprhm  22341  ofco2  22416  basdif0  22918  eltg4i  22925  ntrss2  23022  ntrin  23026  isopn3  23031  resttopon  23126  restuni2  23132  restcld  23137  restfpw  23144  neitr  23145  cnrest2r  23252  cnpresti  23253  cnprest  23254  lmss  23263  cnrmi  23325  restcnrm  23327  resthauslem  23328  imacmp  23362  fiuncmp  23369  subislly  23446  islly2  23449  cldllycmp  23460  hauspwdom  23466  kgeni  23502  llycmpkgen2  23515  ptbasfi  23546  ptclsg  23580  ptcnplem  23586  txtube  23605  txcmplem2  23607  txkgen  23617  kqdisj  23697  fbasrn  23849  trfg  23856  isufil2  23873  fmfnfmlem4  23922  hauspwpwf1  23952  txflf  23971  alexsubALTlem4  24015  tmdgsum2  24061  tsmsres  24109  tsmsxplem1  24118  ustexsym  24181  ustund  24187  trust  24194  utoptop  24199  restutop  24202  metrest  24489  restmetu  24535  tgioo  24761  reconnlem2  24793  cphsqrtcl  25151  tcphcph  25204  cfilresi  25262  caussi  25264  causs  25265  ovolfioo  25434  ovolficc  25435  ovolficcss  25436  ovolfsf  25438  ovollb  25446  ovolicc2lem1  25484  ovolicc2lem2  25485  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2  25489  nulmbl  25502  voliunlem1  25517  ovolfs2  25538  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombllem6  25555  uniioombl  25556  dyadmbllem  25566  dyadmbl  25567  opnmbllem  25568  volcn  25573  volivth  25574  mbfadd  25628  mbfsub  25629  i1fima  25645  i1fima2  25646  i1fd  25648  i1fadd  25662  i1fmul  25663  itg1addlem2  25664  itg1addlem4  25666  itg1addlem5  25667  i1fres  25672  mbfmul  25693  bddmulibl  25806  ellimc2  25844  ellimc3  25846  limcflf  25848  limcresi  25852  limciun  25861  dvreslem  25876  dvres2lem  25877  dvres3a  25881  cpnres  25904  dvaddbr  25905  dvmulbr  25906  dvmptres3  25923  lhop1lem  25980  rlimcnp2  26930  xrlimcnp  26932  chpchtsum  27182  2sqlem8  27389  2sqlem9  27390  rpvmasumlem  27450  rplogsum  27490  dirith2  27491  nosupbnd2  27680  axtgsegcon  28532  axtg5seg  28533  axtgbtwnid  28534  axtgpasch  28535  axtgcont1  28536  tglng  28614  chdmm1i  31548  chm0i  31561  ledii  31607  lejdii  31609  pjoml2i  31656  pjoml4i  31658  cmcmlem  31662  cmbr4i  31672  osumcori  31714  pjssmii  31752  mayete3i  31799  riesz4  32135  riesz1  32136  cnlnadjeu  32149  nmopadjlei  32159  pjclem1  32266  pjci  32271  mdbr3  32368  mdbr4  32369  dmdbr2  32374  dmdbr5  32379  ssmd2  32383  mdslj1i  32390  mdslj2i  32391  mdsl1i  32392  mdsl2bi  32394  mdslmd1lem1  32396  mdslmd1lem2  32397  mdslmd2i  32401  csmdsymi  32405  cvexchlem  32439  atomli  32453  atcvat4i  32468  difininv  32587  disjxpin  32658  imadifxp  32671  off2  32714  mptiffisupp  32766  indsumin  32921  indf1ofs  32926  idlinsubrg  33491  ressply1invg  33629  evls1subd  33632  algextdeglem7  33867  algextdeglem8  33868  ordtrestNEW  34065  pnfneige0  34095  lmxrge0  34096  qqhnm  34134  qqhcn  34135  rrhre  34165  gsumesum  34203  esumlub  34204  esumcst  34207  esumpcvgval  34222  hasheuni  34229  esumcvg  34230  sigainb  34280  carsgclctunlem2  34463  sibfinima  34483  sibfof  34484  eulerpartlemelr  34501  eulerpartlemgh  34522  eulerpartlemgf  34523  eulerpartlemgs2  34524  eulerpartlemn  34525  probmeasb  34574  cndprob01  34579  hashreprin  34764  reprfi2  34767  breprexpnat  34778  hgt750lemd  34792  hgt750lema  34801  tgoldbachgtde  34804  tgoldbachgtda  34805  tgoldbachgt  34807  bnj1293  34958  connpconn  35417  iccllysconn  35432  cvmsss2  35456  cvmcov2  35457  cvmopnlem  35460  cvmliftmolem2  35464  cvmlift2lem12  35496  mvrsfpw  35688  elmsta  35730  msubvrs  35742  mclsind  35752  nepss  35900  dfon2lem4  35966  trer  36498  neiin  36514  neibastop1  36541  neibastop2lem  36542  topmeet  36546  filnetlem3  36562  weiunfr  36649  elttcirr  36713  bj-disj2r  37335  bj-restpw  37404  bj-restb  37406  bj-restuni2  37410  bj-ablsscmn  37592  topdifinffinlem  37663  opnmbllem0  37977  mblfinlem4  37981  mbfposadd  37988  heibor1lem  38130  heiborlem1  38132  heiborlem3  38134  heiborlem10  38141  opidonOLD  38173  disjimin  39172  lshpinN  39435  lcvexchlem1  39480  lcvexchlem5  39484  pmod1i  40294  pmodN  40296  osumcllem7N  40408  pexmidlem4N  40419  dochdmj1  41836  dochexmidlem4  41909  lcfrlem25  42013  mapd1o  42094  mapdin  42108  elrfi  43126  elrfirn  43127  fnwe2lem2  43479  aomclem2  43483  lsmfgcl  43502  lmhmfgima  43512  lmhmfgsplit  43514  lmhmlnmsplit  43515  hbt  43558  ofoafg  43782  trrelind  44092  iunrelexp0  44129  isotone2  44476  grumnudlem  44712  ismnushort  44728  onfrALTlem3  44971  onfrALTlem2  44973  onfrALTlem3VD  45313  onfrALTlem2VD  45315  iunconnlem2  45361  wfac8prim  45429  restuni6  45552  disjinfi  45622  inmap  45638  fsumiunss  46005  islptre  46049  sumnnodd  46060  limcresiooub  46070  limcresioolb  46071  limcleqr  46072  limclner  46079  limclr  46083  limsuplesup  46127  limsuppnfdlem  46129  limsupres  46133  liminfgord  46182  liminfgf  46186  liminfcl  46191  limsupresxr  46194  liminfresxr  46195  liminfval2  46196  liminflelimsuplem  46203  liminfvalxr  46211  icccncfext  46315  fourierdlem20  46555  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem76  46610  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  fouriersw  46659  salgencntex  46771  sge0less  46820  sge0resplit  46834  sge0split  46837  sge0iunmptlemre  46843  sge0fodjrnlem  46844  caragencmpl  46963  ovolval2lem  47071  ovolval2  47072  ovolval3  47075  ovolval4lem2  47078  sssmf  47166  nthrucw  47316  fcoreslem4  47514  fcoresf1  47517  fcoresfo  47519  3f1oss1  47523  rngchomrnghmresALTV  48755  termc  49994