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

This proof depends on syntax axioms:   ∩ cin 3898   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  inindif  4324  vvin  4359  difin0  4428  uniin  4891  iunxdif3  5055  relin2  5791  relres  5996  idssxp  6041  rnin  6137  ssrnres  6170  cnvrescnv  6188  ordin  6392  onfr  6401  ordelinel  6465  fnresin2  6663  fresaunres2  6752  ssimaex  6968  exfo  7103  ffvresb  7124  fnfvimad  7238  ofrfvalg  7699  ofval  7702  ofrval  7703  off  7709  ofres  7710  ofco  7716  fnwelem  8141  fnse  8143  fprlem1  8311  tfrlem5  8380  pmresg  8891  ixpfi2  9332  elfiun  9415  marypha1lem  9418  ordtypelem6  9510  ordtypelem7  9511  hartogslem1  9529  unxpwdom  9576  epfrs  9725  tcmin  9733  bnd2  9949  tskwe  10024  r0weon  10084  infxpenlem  10085  djuinf  10260  ackbij1lem9  10298  ackbij1lem10  10299  ackbij1lem15  10304  ackbij1lem16  10305  ackbij1b  10309  sdom2en01  10373  fin23lem26  10396  fin23lem13  10403  isfin1-3  10457  fin56  10464  fin1a2lem9  10479  brdom3  10600  brdom5  10601  brdom4  10602  fpwwe2lem11  10719  fpwwe2  10721  canthwelem  10728  gruima  10880  ingru  10893  gruina  10896  grur1a  10897  ltrelpi  10967  ltrelnq  11004  nqerf  11008  fzfi  14108  xptrrel  15126  rexanuz  15506  limsupgord  15632  limsupcl  15633  limsupgf  15635  limsupgle  15637  o1of2  15773  o1rlimmul  15779  ackbijnn  15990  bitsinv1  16605  bitsinvp1  16612  sadcaddlem  16620  sadadd2lem  16622  sadadd3  16624  sadaddlem  16629  sadasslem  16633  sadeq  16635  smupval  16651  prmrec  17093  structcnvcnv  17324  ressbasss  17410  ressbasssOLD  17411  ressress  17418  restsspw  17595  submre  17768  isacs1i  17824  rescabs  18001  resscat  18020  funcres2c  18071  ressffth  18108  catccatid  18274  catcisolem  18278  catciso  18279  yoniso  18452  resspos  18596  resstos  18597  acsinfd  18723  acsdomd  18724  tsrss  18756  idresefmnd  19088  idrespermg  19618  mvdco  19652  lsmmod  19882  submomnd  20339  rnghmresfn  20864  rnghmsscmap  20875  rhmresfn  20893  rhmsscmap  20904  rhmsubclem4  20933  acsfn1p  21049  suborng  21126  lssacs  21235  lidlssbas  21485  zringlpirlem2  21762  zringlpirlem3  21763  asplss  22174  ressmplbas  22329  subrgmpl  22333  mplind  22372  ressply1bas  22539  pf1rcl  22660  ressply1evl  22681  evls1addd  22682  evls1muld  22683  evls1vsca  22684  evls1maprhm  22687  ofco2  22759  basdif0  23264  eltg4i  23271  ntrss2  23368  ntrin  23372  isopn3  23377  resttopon  23472  restuni2  23478  restcld  23483  restfpw  23490  neitr  23491  cnrest2r  23598  cnpresti  23599  cnprest  23600  lmss  23609  cnrmi  23671  restcnrm  23673  resthauslem  23674  imacmp  23708  fiuncmp  23715  subislly  23793  islly2  23796  cldllycmp  23807  hauspwdom  23813  kgeni  23849  llycmpkgen2  23862  ptbasfi  23893  ptclsg  23927  ptcnplem  23933  txtube  23952  txcmplem2  23954  txkgen  23964  kqdisj  24044  fbasrn  24196  trfg  24203  isufil2  24220  fmfnfmlem4  24269  hauspwpwf1  24299  txflf  24318  alexsubALTlem4  24362  tmdgsum2  24408  tsmsres  24456  tsmsxplem1  24465  ustexsym  24528  ustund  24534  trust  24541  utoptop  24546  restutop  24549  metrest  24836  restmetu  24882  tgioo  25108  reconnlem2  25140  cphsqrtcl  25498  tcphcph  25551  cfilresi  25609  caussi  25611  causs  25612  ovolfioo  25781  ovolficc  25782  ovolficcss  25783  ovolfsf  25785  ovollb  25793  ovolicc2lem1  25831  ovolicc2lem2  25832  ovolicc2lem3  25833  ovolicc2lem4  25834  ovolicc2  25836  nulmbl  25849  voliunlem1  25864  ovolfs2  25885  uniiccdif  25892  uniioovol  25893  uniiccvol  25894  uniioombllem2  25897  uniioombllem3a  25898  uniioombllem3  25899  uniioombllem4  25900  uniioombllem5  25901  uniioombllem6  25902  uniioombl  25903  dyadmbllem  25913  dyadmbl  25914  opnmbllem  25915  volcn  25920  volivth  25921  mbfadd  25975  mbfsub  25976  i1fima  25992  i1fima2  25993  i1fd  25995  i1fadd  26009  i1fmul  26010  itg1addlem2  26011  itg1addlem4  26013  itg1addlem5  26014  i1fres  26019  mbfmul  26040  bddmulibl  26152  ellimc2  26190  ellimc3  26192  limcflf  26194  limcresi  26198  limciun  26207  dvreslem  26222  dvres2lem  26223  dvres3a  26227  cpnres  26250  dvaddbr  26251  dvmulbr  26252  dvmptres3  26269  lhop1lem  26326  rlimcnp2  27287  xrlimcnp  27289  chpchtsum  27539  2sqlem8  27746  2sqlem9  27747  rpvmasumlem  27807  rplogsum  27847  dirith2  27848  nosupbnd2  28066  axtgsegcon  28919  axtg5seg  28920  axtgbtwnid  28921  axtgpasch  28922  axtgcont1  28923  tglng  29002  chdmm1i  32072  chm0i  32085  ledii  32131  lejdii  32133  pjoml2i  32180  pjoml4i  32182  cmcmlem  32186  cmbr4i  32196  osumcori  32238  pjssmii  32276  mayete3i  32323  riesz4  32659  riesz1  32660  cnlnadjeu  32673  nmopadjlei  32683  pjclem1  32790  pjci  32795  mdbr3  32892  mdbr4  32893  dmdbr2  32898  dmdbr5  32903  ssmd2  32907  mdslj1i  32914  mdslj2i  32915  mdsl1i  32916  mdsl2bi  32918  mdslmd1lem1  32920  mdslmd1lem2  32921  mdslmd2i  32925  csmdsymi  32929  cvexchlem  32963  atomli  32977  atcvat4i  32992  difininv  33106  disjxpin  33175  imadifxp  33188  off2  33228  mptiffisupp  33279  indsumin  33421  indf1ofs  33426  idlinsubrg  33974  ressply1invg  34094  evls1subd  34097  algextdeglem7  34348  algextdeglem8  34349  ordtrestNEW  34546  pnfneige0  34576  lmxrge0  34577  qqhnm  34615  qqhcn  34616  rrhre  34646  gsumesum  34684  esumlub  34685  esumcst  34688  esumpcvgval  34703  hasheuni  34710  esumcvg  34711  sigainb  34762  carsgclctunlem2  34944  sibfinima  34964  sibfof  34965  eulerpartlemelr  34982  eulerpartlemgh  35003  eulerpartlemgf  35004  eulerpartlemgs2  35005  eulerpartlemn  35006  probmeasb  35055  cndprob01  35060  hashreprin  35242  reprfi2  35245  breprexpnat  35256  hgt750lemd  35270  hgt750lema  35279  tgoldbachgtde  35282  tgoldbachgtda  35283  tgoldbachgt  35285  bnj1293  35439  connpconn  35979  iccllysconn  35994  cvmsss2  36018  cvmcov2  36019  cvmopnlem  36022  cvmliftmolem2  36026  cvmlift2lem12  36058  mvrsfpw  36250  elmsta  36292  msubvrs  36304  mclsind  36314  nepss  36462  dfon2lem4  36528  trer  37084  neiin  37100  neibastop1  37127  neibastop2lem  37128  topmeet  37132  filnetlem3  37148  weiunfr  37235  elttcirr  37299  bj-disj2r  37921  bj-restpw  37993  bj-restb  37995  bj-restuni2  37999  bj-ablsscmn  38179  topdifinffinlem  38250  opnmbllem0  38554  mblfinlem4  38558  mbfposadd  38565  heibor1lem  38723  heiborlem1  38725  heiborlem3  38727  heiborlem10  38734  opidonOLD  38766  disjimin  39763  lshpinN  40026  lcvexchlem1  40071  lcvexchlem5  40075  pmod1i  40885  pmodN  40887  osumcllem7N  40999  pexmidlem4N  41010  dochdmj1  42427  dochexmidlem4  42500  lcfrlem25  42604  mapd1o  42685  mapdin  42699  elrfi  43684  elrfirn  43685  fnwe2lem2  44037  aomclem2  44041  lsmfgcl  44060  lmhmfgima  44070  lmhmfgsplit  44072  lmhmlnmsplit  44073  hbt  44116  ofoafg  44340  trrelind  44650  iunrelexp0  44687  isotone2  45034  grumnudlem  45254  ismnushort  45270  onfrALTlem3  45512  onfrALTlem2  45514  onfrALTlem3VD  45854  onfrALTlem2VD  45856  iunconnlem2  45902  wfac8prim  45970  restuni6  46106  disjinfi  46176  inmap  46191  fsumiunss  46556  islptre  46600  sumnnodd  46611  limcresiooub  46621  limcresioolb  46622  limcleqr  46623  limclner  46630  limclr  46634  limsuplesup  46678  limsuppnfdlem  46680  limsupres  46684  liminfgord  46733  liminfgf  46737  liminfcl  46742  limsupresxr  46745  liminfresxr  46746  liminfval2  46747  liminflelimsuplem  46754  liminfvalxr  46762  icccncfext  46866  fourierdlem20  47106  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem76  47161  fourierdlem103  47188  fourierdlem104  47189  fourierdlem113  47198  fouriersw  47210  salgencntex  47322  sge0less  47371  sge0resplit  47385  sge0split  47388  sge0iunmptlemre  47394  sge0fodjrnlem  47395  caragencmpl  47514  ovolval2lem  47622  ovolval2  47623  ovolval3  47626  ovolval4lem2  47629  sssmf  47717  wrddrin  47866  chndrin  47871  chnrrin  47876  numtowerdt  47885  tmachlem-fssscan  47929  fcoreslem4  48105  fcoresf1  48108  fcoresfo  48110  3f1oss1  48114  rngchomrnghmresALTV  49345  termc  50596