Theorem inss2 4183

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 4154	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4182	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3977	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3896   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  inindif  4320  difin0  4419  iunxdif3  5038  relin2  5748  relres  5949  idssxp  5993  ssrnres  6120  cnvrescnv  6137  ordin  6331  onfr  6340  ordelinel  6404  fnresin2  6602  fresaunres2  6690  ssimaex  6902  exfo  7033  ffvresb  7053  fnfvimad  7163  ofrfvalg  7613  ofval  7616  ofrval  7617  off  7623  ofres  7624  ofco  7630  fnwelem  8056  fnse  8058  fprlem1  8225  tfrlem5  8294  pmresg  8789  ixpfi2  9229  elfiun  9309  marypha1lem  9312  ordtypelem6  9404  ordtypelem7  9405  hartogslem1  9423  unxpwdom  9470  epfrs  9616  tcmin  9624  bnd2  9781  tskwe  9838  r0weon  9898  infxpenlem  9899  djuinf  10075  ackbij1lem9  10113  ackbij1lem10  10114  ackbij1lem15  10119  ackbij1lem16  10120  ackbij1b  10124  sdom2en01  10188  fin23lem26  10211  fin23lem13  10218  isfin1-3  10272  fin56  10279  fin1a2lem9  10294  brdom3  10414  brdom5  10415  brdom4  10416  fpwwe2lem11  10527  fpwwe2  10529  canthwelem  10536  gruima  10688  ingru  10701  gruina  10704  grur1a  10705  ltrelpi  10775  ltrelnq  10812  nqerf  10816  fzfi  13874  xptrrel  14882  rexanuz  15248  limsupgord  15374  limsupcl  15375  limsupgf  15377  limsupgle  15379  o1of2  15515  o1rlimmul  15521  ackbijnn  15730  bitsinv1  16348  bitsinvp1  16355  sadcaddlem  16363  sadadd2lem  16365  sadadd3  16367  sadaddlem  16372  sadasslem  16376  sadeq  16378  smupval  16394  prmrec  16829  structcnvcnv  17059  ressbasss  17145  ressbasssOLD  17146  ressress  17153  restsspw  17330  submre  17502  isacs1i  17558  rescabs  17735  resscat  17754  funcres2c  17805  ressffth  17842  catccatid  18008  catcisolem  18012  catciso  18013  yoniso  18186  resspos  18330  resstos  18331  acsinfd  18457  acsdomd  18458  tsrss  18490  idresefmnd  18802  idrespermg  19318  mvdco  19352  lsmmod  19582  submomnd  20039  rnghmresfn  20529  rnghmsscmap  20540  rhmresfn  20558  rhmsscmap  20569  rhmsubclem4  20598  acsfn1p  20709  suborng  20786  lssacs  20895  lidlssbas  21145  zringlpirlem2  21395  zringlpirlem3  21396  asplss  21806  ressmplbas  21958  subrgmpl  21962  mplind  22000  ressply1bas  22136  pf1rcl  22259  ressply1evl  22280  evls1addd  22281  evls1muld  22282  evls1vsca  22283  evls1maprhm  22286  ofco2  22361  basdif0  22863  eltg4i  22870  ntrss2  22967  ntrin  22971  isopn3  22976  resttopon  23071  restuni2  23077  restcld  23082  restfpw  23089  neitr  23090  cnrest2r  23197  cnpresti  23198  cnprest  23199  lmss  23208  cnrmi  23270  restcnrm  23272  resthauslem  23273  imacmp  23307  fiuncmp  23314  subislly  23391  islly2  23394  cldllycmp  23405  hauspwdom  23411  kgeni  23447  llycmpkgen2  23460  ptbasfi  23491  ptclsg  23525  ptcnplem  23531  txtube  23550  txcmplem2  23552  txkgen  23562  kqdisj  23642  fbasrn  23794  trfg  23801  isufil2  23818  fmfnfmlem4  23867  hauspwpwf1  23897  txflf  23916  alexsubALTlem4  23960  tmdgsum2  24006  tsmsres  24054  tsmsxplem1  24063  ustexsym  24126  ustund  24132  trust  24139  utoptop  24144  restutop  24147  metrest  24434  restmetu  24480  tgioo  24706  reconnlem2  24738  cphsqrtcl  25106  tcphcph  25159  cfilresi  25217  caussi  25219  causs  25220  ovolfioo  25390  ovolficc  25391  ovolficcss  25392  ovolfsf  25394  ovollb  25402  ovolicc2lem1  25440  ovolicc2lem2  25441  ovolicc2lem3  25442  ovolicc2lem4  25443  ovolicc2  25445  nulmbl  25458  voliunlem1  25473  ovolfs2  25494  uniiccdif  25501  uniioovol  25502  uniiccvol  25503  uniioombllem2  25506  uniioombllem3a  25507  uniioombllem3  25508  uniioombllem4  25509  uniioombllem5  25510  uniioombllem6  25511  uniioombl  25512  dyadmbllem  25522  dyadmbl  25523  opnmbllem  25524  volcn  25529  volivth  25530  mbfadd  25584  mbfsub  25585  i1fima  25601  i1fima2  25602  i1fd  25604  i1fadd  25618  i1fmul  25619  itg1addlem2  25620  itg1addlem4  25622  itg1addlem5  25623  i1fres  25628  mbfmul  25649  bddmulibl  25762  ellimc2  25800  ellimc3  25802  limcflf  25804  limcresi  25808  limciun  25817  dvreslem  25832  dvres2lem  25833  dvres3a  25837  cpnres  25861  dvaddbr  25862  dvmulbr  25863  dvmulbrOLD  25864  dvmptres3  25882  lhop1lem  25940  rlimcnp2  26898  xrlimcnp  26900  chpchtsum  27152  2sqlem8  27359  2sqlem9  27360  rpvmasumlem  27420  rplogsum  27460  dirith2  27461  nosupbnd2  27650  axtgsegcon  28437  axtg5seg  28438  axtgbtwnid  28439  axtgpasch  28440  axtgcont1  28441  tglng  28519  chdmm1i  31449  chm0i  31462  ledii  31508  lejdii  31510  pjoml2i  31557  pjoml4i  31559  cmcmlem  31563  cmbr4i  31573  osumcori  31615  pjssmii  31653  mayete3i  31700  riesz4  32036  riesz1  32037  cnlnadjeu  32050  nmopadjlei  32060  pjclem1  32167  pjci  32172  mdbr3  32269  mdbr4  32270  dmdbr2  32275  dmdbr5  32280  ssmd2  32284  mdslj1i  32291  mdslj2i  32292  mdsl1i  32293  mdsl2bi  32295  mdslmd1lem1  32297  mdslmd1lem2  32298  mdslmd2i  32302  csmdsymi  32306  cvexchlem  32340  atomli  32354  atcvat4i  32369  difininv  32489  disjxpin  32560  imadifxp  32573  off2  32615  mptiffisupp  32666  indsumin  32835  indf1ofs  32839  idlinsubrg  33388  ressply1invg  33524  evls1subd  33527  algextdeglem7  33728  algextdeglem8  33729  ordtrestNEW  33926  pnfneige0  33956  lmxrge0  33957  qqhnm  33995  qqhcn  33996  rrhre  34026  gsumesum  34064  esumlub  34065  esumcst  34068  esumpcvgval  34083  hasheuni  34090  esumcvg  34091  sigainb  34141  carsgclctunlem2  34324  sibfinima  34344  sibfof  34345  eulerpartlemelr  34362  eulerpartlemgh  34383  eulerpartlemgf  34384  eulerpartlemgs2  34385  eulerpartlemn  34386  probmeasb  34435  cndprob01  34440  hashreprin  34625  reprfi2  34628  breprexpnat  34639  hgt750lemd  34653  hgt750lema  34662  tgoldbachgtde  34665  tgoldbachgtda  34666  tgoldbachgt  34668  bnj1293  34820  connpconn  35271  iccllysconn  35286  cvmsss2  35310  cvmcov2  35311  cvmopnlem  35314  cvmliftmolem2  35318  cvmlift2lem12  35350  mvrsfpw  35542  elmsta  35584  msubvrs  35596  mclsind  35606  nepss  35754  dfon2lem4  35820  trer  36350  neiin  36366  neibastop1  36393  neibastop2lem  36394  topmeet  36398  filnetlem3  36414  weiunfr  36501  bj-disj2r  37062  bj-restpw  37126  bj-restb  37128  bj-restuni2  37132  bj-ablsscmn  37312  topdifinffinlem  37381  opnmbllem0  37696  mblfinlem4  37700  mbfposadd  37707  heibor1lem  37849  heiborlem1  37851  heiborlem3  37853  heiborlem10  37860  opidonOLD  37892  disjimin  38789  lshpinN  39028  lcvexchlem1  39073  lcvexchlem5  39077  pmod1i  39887  pmodN  39889  osumcllem7N  40001  pexmidlem4N  40012  dochdmj1  41429  dochexmidlem4  41502  lcfrlem25  41606  mapd1o  41687  mapdin  41701  elrfi  42727  elrfirn  42728  fnwe2lem2  43084  aomclem2  43088  lsmfgcl  43107  lmhmfgima  43117  lmhmfgsplit  43119  lmhmlnmsplit  43120  hbt  43163  ofoafg  43387  trrelind  43698  iunrelexp0  43735  isotone2  44082  grumnudlem  44318  ismnushort  44334  onfrALTlem3  44577  onfrALTlem2  44579  onfrALTlem3VD  44919  onfrALTlem2VD  44921  iunconnlem2  44967  wfac8prim  45035  restuni6  45159  disjinfi  45229  inmap  45246  fsumiunss  45615  islptre  45659  sumnnodd  45670  limcresiooub  45680  limcresioolb  45681  limcleqr  45682  limclner  45689  limclr  45693  limsuplesup  45737  limsuppnfdlem  45739  limsupres  45743  liminfgord  45792  liminfgf  45796  liminfcl  45801  limsupresxr  45804  liminfresxr  45805  liminfval2  45806  liminflelimsuplem  45813  liminfvalxr  45821  icccncfext  45925  fourierdlem20  46165  fourierdlem48  46192  fourierdlem49  46193  fourierdlem50  46194  fourierdlem76  46220  fourierdlem103  46247  fourierdlem104  46248  fourierdlem113  46257  fouriersw  46269  salgencntex  46381  sge0less  46430  sge0resplit  46444  sge0split  46447  sge0iunmptlemre  46453  sge0fodjrnlem  46454  caragencmpl  46573  ovolval2lem  46681  ovolval2  46682  ovolval3  46685  ovolval4lem2  46688  sssmf  46776  fcoreslem4  47097  fcoresf1  47100  fcoresfo  47102  3f1oss1  47106  rngchomrnghmresALTV  48310  termc  49551