Theorem inss2 4166

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 4138	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4165	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3962	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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900

This theorem is referenced by:  inindif  4303  difin0  4402  iunxdif3  5024  relin2  5756  relres  5957  idssxp  6001  ssrnres  6129  cnvrescnv  6146  ordin  6340  onfr  6349  ordelinel  6413  fnresin2  6611  fresaunres2  6699  ssimaex  6912  exfo  7046  ffvresb  7067  fnfvimad  7178  ofrfvalg  7628  ofval  7631  ofrval  7632  off  7638  ofres  7639  ofco  7645  fnwelem  8071  fnse  8073  fprlem1  8240  tfrlem5  8309  pmresg  8808  ixpfi2  9250  elfiun  9333  marypha1lem  9336  ordtypelem6  9428  ordtypelem7  9429  hartogslem1  9447  unxpwdom  9494  epfrs  9643  tcmin  9651  bnd2  9808  tskwe  9865  r0weon  9925  infxpenlem  9926  djuinf  10102  ackbij1lem9  10140  ackbij1lem10  10141  ackbij1lem15  10146  ackbij1lem16  10147  ackbij1b  10151  sdom2en01  10215  fin23lem26  10238  fin23lem13  10245  isfin1-3  10299  fin56  10306  fin1a2lem9  10321  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem11  10555  fpwwe2  10557  canthwelem  10564  gruima  10716  ingru  10729  gruina  10732  grur1a  10733  ltrelpi  10803  ltrelnq  10840  nqerf  10844  fzfi  13925  xptrrel  14933  rexanuz  15299  limsupgord  15425  limsupcl  15426  limsupgf  15428  limsupgle  15430  o1of2  15566  o1rlimmul  15572  ackbijnn  15784  bitsinv1  16402  bitsinvp1  16409  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  smupval  16448  prmrec  16884  structcnvcnv  17114  ressbasss  17200  ressbasssOLD  17201  ressress  17208  restsspw  17385  submre  17558  isacs1i  17614  rescabs  17791  resscat  17810  funcres2c  17861  ressffth  17898  catccatid  18064  catcisolem  18068  catciso  18069  yoniso  18242  resspos  18386  resstos  18387  acsinfd  18513  acsdomd  18514  tsrss  18546  idresefmnd  18858  idrespermg  19377  mvdco  19411  lsmmod  19641  submomnd  20098  rnghmresfn  20591  rnghmsscmap  20602  rhmresfn  20620  rhmsscmap  20631  rhmsubclem4  20660  acsfn1p  20771  suborng  20848  lssacs  20957  lidlssbas  21206  zringlpirlem2  21438  zringlpirlem3  21439  asplss  21848  ressmplbas  22003  subrgmpl  22007  mplind  22046  ressply1bas  22213  pf1rcl  22335  ressply1evl  22356  evls1addd  22357  evls1muld  22358  evls1vsca  22359  evls1maprhm  22362  ofco2  22434  basdif0  22936  eltg4i  22943  ntrss2  23040  ntrin  23044  isopn3  23049  resttopon  23144  restuni2  23150  restcld  23155  restfpw  23162  neitr  23163  cnrest2r  23270  cnpresti  23271  cnprest  23272  lmss  23281  cnrmi  23343  restcnrm  23345  resthauslem  23346  imacmp  23380  fiuncmp  23387  subislly  23464  islly2  23467  cldllycmp  23478  hauspwdom  23484  kgeni  23520  llycmpkgen2  23533  ptbasfi  23564  ptclsg  23598  ptcnplem  23604  txtube  23623  txcmplem2  23625  txkgen  23635  kqdisj  23715  fbasrn  23867  trfg  23874  isufil2  23891  fmfnfmlem4  23940  hauspwpwf1  23970  txflf  23989  alexsubALTlem4  24033  tmdgsum2  24079  tsmsres  24127  tsmsxplem1  24136  ustexsym  24199  ustund  24205  trust  24212  utoptop  24217  restutop  24220  metrest  24507  restmetu  24553  tgioo  24779  reconnlem2  24811  cphsqrtcl  25169  tcphcph  25222  cfilresi  25280  caussi  25282  causs  25283  ovolfioo  25452  ovolficc  25453  ovolficcss  25454  ovolfsf  25456  ovollb  25464  ovolicc2lem1  25502  ovolicc2lem2  25503  ovolicc2lem3  25504  ovolicc2lem4  25505  ovolicc2  25507  nulmbl  25520  voliunlem1  25535  ovolfs2  25556  uniiccdif  25563  uniioovol  25564  uniiccvol  25565  uniioombllem2  25568  uniioombllem3a  25569  uniioombllem3  25570  uniioombllem4  25571  uniioombllem5  25572  uniioombllem6  25573  uniioombl  25574  dyadmbllem  25584  dyadmbl  25585  opnmbllem  25586  volcn  25591  volivth  25592  mbfadd  25646  mbfsub  25647  i1fima  25663  i1fima2  25664  i1fd  25666  i1fadd  25680  i1fmul  25681  itg1addlem2  25682  itg1addlem4  25684  itg1addlem5  25685  i1fres  25690  mbfmul  25711  bddmulibl  25824  ellimc2  25862  ellimc3  25864  limcflf  25866  limcresi  25870  limciun  25879  dvreslem  25894  dvres2lem  25895  dvres3a  25899  cpnres  25922  dvaddbr  25923  dvmulbr  25924  dvmptres3  25941  lhop1lem  25998  rlimcnp2  26948  xrlimcnp  26950  chpchtsum  27200  2sqlem8  27407  2sqlem9  27408  rpvmasumlem  27468  rplogsum  27508  dirith2  27509  nosupbnd2  27698  axtgsegcon  28550  axtg5seg  28551  axtgbtwnid  28552  axtgpasch  28553  axtgcont1  28554  tglng  28632  chdmm1i  31566  chm0i  31579  ledii  31625  lejdii  31627  pjoml2i  31674  pjoml4i  31676  cmcmlem  31680  cmbr4i  31690  osumcori  31732  pjssmii  31770  mayete3i  31817  riesz4  32153  riesz1  32154  cnlnadjeu  32167  nmopadjlei  32177  pjclem1  32284  pjci  32289  mdbr3  32386  mdbr4  32387  dmdbr2  32392  dmdbr5  32397  ssmd2  32401  mdslj1i  32408  mdslj2i  32409  mdsl1i  32410  mdsl2bi  32412  mdslmd1lem1  32414  mdslmd1lem2  32415  mdslmd2i  32419  csmdsymi  32423  cvexchlem  32457  atomli  32471  atcvat4i  32486  difininv  32605  disjxpin  32677  imadifxp  32690  off2  32733  mptiffisupp  32785  indsumin  32940  indf1ofs  32945  idlinsubrg  33514  ressply1invg  33652  evls1subd  33655  algextdeglem7  33907  algextdeglem8  33908  ordtrestNEW  34105  pnfneige0  34135  lmxrge0  34136  qqhnm  34174  qqhcn  34175  rrhre  34205  gsumesum  34243  esumlub  34244  esumcst  34247  esumpcvgval  34262  hasheuni  34269  esumcvg  34270  sigainb  34320  carsgclctunlem2  34503  sibfinima  34523  sibfof  34524  eulerpartlemelr  34541  eulerpartlemgh  34562  eulerpartlemgf  34563  eulerpartlemgs2  34564  eulerpartlemn  34565  probmeasb  34614  cndprob01  34619  hashreprin  34804  reprfi2  34807  breprexpnat  34818  hgt750lemd  34832  hgt750lema  34841  tgoldbachgtde  34844  tgoldbachgtda  34845  tgoldbachgt  34847  bnj1293  34998  connpconn  35463  iccllysconn  35478  cvmsss2  35502  cvmcov2  35503  cvmopnlem  35506  cvmliftmolem2  35510  cvmlift2lem12  35542  mvrsfpw  35734  elmsta  35776  msubvrs  35788  mclsind  35798  nepss  35946  dfon2lem4  36012  trer  36544  neiin  36560  neibastop1  36587  neibastop2lem  36588  topmeet  36592  filnetlem3  36608  weiunfr  36695  elttcirr  36759  bj-disj2r  37381  bj-restpw  37450  bj-restb  37452  bj-restuni2  37456  bj-ablsscmn  37638  topdifinffinlem  37709  opnmbllem0  38023  mblfinlem4  38027  mbfposadd  38034  heibor1lem  38176  heiborlem1  38178  heiborlem3  38180  heiborlem10  38187  opidonOLD  38219  disjimin  39218  lshpinN  39481  lcvexchlem1  39526  lcvexchlem5  39530  pmod1i  40340  pmodN  40342  osumcllem7N  40454  pexmidlem4N  40465  dochdmj1  41882  dochexmidlem4  41955  lcfrlem25  42059  mapd1o  42140  mapdin  42154  elrfi  43143  elrfirn  43144  fnwe2lem2  43496  aomclem2  43500  lsmfgcl  43519  lmhmfgima  43529  lmhmfgsplit  43531  lmhmlnmsplit  43532  hbt  43575  ofoafg  43799  trrelind  44109  iunrelexp0  44146  isotone2  44493  grumnudlem  44729  ismnushort  44745  onfrALTlem3  44988  onfrALTlem2  44990  onfrALTlem3VD  45330  onfrALTlem2VD  45332  iunconnlem2  45378  wfac8prim  45446  restuni6  45569  disjinfi  45639  inmap  45654  fsumiunss  46020  islptre  46064  sumnnodd  46075  limcresiooub  46085  limcresioolb  46086  limcleqr  46087  limclner  46094  limclr  46098  limsuplesup  46142  limsuppnfdlem  46144  limsupres  46148  liminfgord  46197  liminfgf  46201  liminfcl  46206  limsupresxr  46209  liminfresxr  46210  liminfval2  46211  liminflelimsuplem  46218  liminfvalxr  46226  icccncfext  46330  fourierdlem20  46570  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem76  46625  fourierdlem103  46652  fourierdlem104  46653  fourierdlem113  46662  fouriersw  46674  salgencntex  46786  sge0less  46835  sge0resplit  46849  sge0split  46852  sge0iunmptlemre  46858  sge0fodjrnlem  46859  caragencmpl  46978  ovolval2lem  47086  ovolval2  47087  ovolval3  47090  ovolval4lem2  47093  sssmf  47181  nthrucw  47331  fcoreslem4  47529  fcoresf1  47532  fcoresfo  47534  3f1oss1  47538  rngchomrnghmresALTV  48770  termc  50009