Theorem inss2 4190

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 4162	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4189	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3984	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3904   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922

This theorem is referenced by:  inindif  4331  vvin  4366  difin0  4435  uniin  4896  iunxdif3  5061  relin2  5800  relres  6004  idssxp  6051  rnin  6143  ssrnres  6176  cnvrescnv  6194  ordin  6391  onfr  6400  ordelinel  6464  fnresin2  6661  fresaunres2  6750  ssimaex  6966  exfo  7100  ffvresb  7121  fnfvimad  7232  ofrfvalg  7682  ofval  7685  ofrval  7686  off  7692  ofres  7693  ofco  7699  fnwelem  8123  fnse  8125  fprlem1  8293  tfrlem5  8362  pmresg  8864  ixpfi2  9303  elfiun  9386  marypha1lem  9389  ordtypelem6  9481  ordtypelem7  9482  hartogslem1  9500  unxpwdom  9547  epfrs  9696  tcmin  9704  bnd2  9875  tskwe  9932  r0weon  9992  infxpenlem  9993  djuinf  10168  ackbij1lem9  10206  ackbij1lem10  10207  ackbij1lem15  10212  ackbij1lem16  10213  ackbij1b  10217  sdom2en01  10281  fin23lem26  10304  fin23lem13  10311  isfin1-3  10365  fin56  10372  fin1a2lem9  10387  brdom3  10507  brdom5  10508  brdom4  10509  fpwwe2lem11  10621  fpwwe2  10623  canthwelem  10630  gruima  10782  ingru  10795  gruina  10798  grur1a  10799  ltrelpi  10869  ltrelnq  10906  nqerf  10910  fzfi  14004  xptrrel  15013  rexanuz  15393  limsupgord  15519  limsupcl  15520  limsupgf  15522  limsupgle  15524  o1of2  15660  o1rlimmul  15666  ackbijnn  15878  bitsinv1  16495  bitsinvp1  16502  sadcaddlem  16510  sadadd2lem  16512  sadadd3  16514  sadaddlem  16519  sadasslem  16523  sadeq  16525  smupval  16541  prmrec  16977  structcnvcnv  17208  ressbasss  17294  ressbasssOLD  17295  ressress  17302  restsspw  17479  submre  17652  isacs1i  17708  rescabs  17885  resscat  17904  funcres2c  17955  ressffth  17992  catccatid  18158  catcisolem  18162  catciso  18163  yoniso  18336  resspos  18480  resstos  18481  acsinfd  18607  acsdomd  18608  tsrss  18640  idresefmnd  18953  idrespermg  19476  mvdco  19510  lsmmod  19740  submomnd  20197  rnghmresfn  20718  rnghmsscmap  20729  rhmresfn  20747  rhmsscmap  20758  rhmsubclem4  20787  acsfn1p  20902  suborng  20979  lssacs  21088  lidlssbas  21338  zringlpirlem2  21613  zringlpirlem3  21614  asplss  22023  ressmplbas  22178  subrgmpl  22182  mplind  22221  ressply1bas  22388  pf1rcl  22509  ressply1evl  22530  evls1addd  22531  evls1muld  22532  evls1vsca  22533  evls1maprhm  22536  ofco2  22608  basdif0  23110  eltg4i  23117  ntrss2  23214  ntrin  23218  isopn3  23223  resttopon  23318  restuni2  23324  restcld  23329  restfpw  23336  neitr  23337  cnrest2r  23444  cnpresti  23445  cnprest  23446  lmss  23455  cnrmi  23517  restcnrm  23519  resthauslem  23520  imacmp  23554  fiuncmp  23561  subislly  23638  islly2  23641  cldllycmp  23652  hauspwdom  23658  kgeni  23694  llycmpkgen2  23707  ptbasfi  23738  ptclsg  23772  ptcnplem  23778  txtube  23797  txcmplem2  23799  txkgen  23809  kqdisj  23889  fbasrn  24041  trfg  24048  isufil2  24065  fmfnfmlem4  24114  hauspwpwf1  24144  txflf  24163  alexsubALTlem4  24207  tmdgsum2  24253  tsmsres  24301  tsmsxplem1  24310  ustexsym  24373  ustund  24379  trust  24386  utoptop  24391  restutop  24394  metrest  24681  restmetu  24727  tgioo  24953  reconnlem2  24985  cphsqrtcl  25343  tcphcph  25396  cfilresi  25454  caussi  25456  causs  25457  ovolfioo  25626  ovolficc  25627  ovolficcss  25628  ovolfsf  25630  ovollb  25638  ovolicc2lem1  25676  ovolicc2lem2  25677  ovolicc2lem3  25678  ovolicc2lem4  25679  ovolicc2  25681  nulmbl  25694  voliunlem1  25709  ovolfs2  25730  uniiccdif  25737  uniioovol  25738  uniiccvol  25739  uniioombllem2  25742  uniioombllem3a  25743  uniioombllem3  25744  uniioombllem4  25745  uniioombllem5  25746  uniioombllem6  25747  uniioombl  25748  dyadmbllem  25758  dyadmbl  25759  opnmbllem  25760  volcn  25765  volivth  25766  mbfadd  25820  mbfsub  25821  i1fima  25837  i1fima2  25838  i1fd  25840  i1fadd  25854  i1fmul  25855  itg1addlem2  25856  itg1addlem4  25858  itg1addlem5  25859  i1fres  25864  mbfmul  25885  bddmulibl  25998  ellimc2  26036  ellimc3  26038  limcflf  26040  limcresi  26044  limciun  26053  dvreslem  26068  dvres2lem  26069  dvres3a  26073  cpnres  26096  dvaddbr  26097  dvmulbr  26098  dvmptres3  26115  lhop1lem  26172  rlimcnp2  27131  xrlimcnp  27133  chpchtsum  27383  2sqlem8  27590  2sqlem9  27591  rpvmasumlem  27651  rplogsum  27691  dirith2  27692  nosupbnd2  27880  axtgsegcon  28733  axtg5seg  28734  axtgbtwnid  28735  axtgpasch  28736  axtgcont1  28737  tglng  28815  chdmm1i  31829  chm0i  31842  ledii  31888  lejdii  31890  pjoml2i  31937  pjoml4i  31939  cmcmlem  31943  cmbr4i  31953  osumcori  31995  pjssmii  32033  mayete3i  32080  riesz4  32416  riesz1  32417  cnlnadjeu  32430  nmopadjlei  32440  pjclem1  32547  pjci  32552  mdbr3  32649  mdbr4  32650  dmdbr2  32655  dmdbr5  32660  ssmd2  32664  mdslj1i  32671  mdslj2i  32672  mdsl1i  32673  mdsl2bi  32675  mdslmd1lem1  32677  mdslmd1lem2  32678  mdslmd2i  32682  csmdsymi  32686  cvexchlem  32720  atomli  32734  atcvat4i  32749  difininv  32863  disjxpin  32933  imadifxp  32946  off2  32986  mptiffisupp  33038  indsumin  33181  indf1ofs  33186  idlinsubrg  33739  ressply1invg  33859  evls1subd  33862  algextdeglem7  34113  algextdeglem8  34114  ordtrestNEW  34311  pnfneige0  34341  lmxrge0  34342  qqhnm  34380  qqhcn  34381  rrhre  34411  gsumesum  34449  esumlub  34450  esumcst  34453  esumpcvgval  34468  hasheuni  34475  esumcvg  34476  sigainb  34526  carsgclctunlem2  34709  sibfinima  34729  sibfof  34730  eulerpartlemelr  34747  eulerpartlemgh  34768  eulerpartlemgf  34769  eulerpartlemgs2  34770  eulerpartlemn  34771  probmeasb  34820  cndprob01  34825  hashreprin  35007  reprfi2  35010  breprexpnat  35021  hgt750lemd  35035  hgt750lema  35044  tgoldbachgtde  35047  tgoldbachgtda  35048  tgoldbachgt  35050  bnj1293  35204  connpconn  35727  iccllysconn  35742  cvmsss2  35766  cvmcov2  35767  cvmopnlem  35770  cvmliftmolem2  35774  cvmlift2lem12  35806  mvrsfpw  35998  elmsta  36040  msubvrs  36052  mclsind  36062  nepss  36210  dfon2lem4  36276  trer  36827  neiin  36843  neibastop1  36870  neibastop2lem  36871  topmeet  36875  filnetlem3  36891  weiunfr  36978  elttcirr  37042  bj-disj2r  37664  bj-restpw  37734  bj-restb  37736  bj-restuni2  37740  bj-ablsscmn  37922  topdifinffinlem  37993  opnmbllem0  38307  mblfinlem4  38311  mbfposadd  38318  heibor1lem  38460  heiborlem1  38462  heiborlem3  38464  heiborlem10  38471  opidonOLD  38503  disjimin  39500  lshpinN  39763  lcvexchlem1  39808  lcvexchlem5  39812  pmod1i  40622  pmodN  40624  osumcllem7N  40736  pexmidlem4N  40747  dochdmj1  42164  dochexmidlem4  42237  lcfrlem25  42341  mapd1o  42422  mapdin  42436  elrfi  43425  elrfirn  43426  fnwe2lem2  43778  aomclem2  43782  lsmfgcl  43801  lmhmfgima  43811  lmhmfgsplit  43813  lmhmlnmsplit  43814  hbt  43857  ofoafg  44081  trrelind  44391  iunrelexp0  44428  isotone2  44775  grumnudlem  44995  ismnushort  45011  onfrALTlem3  45253  onfrALTlem2  45255  onfrALTlem3VD  45595  onfrALTlem2VD  45597  iunconnlem2  45643  wfac8prim  45711  restuni6  45840  disjinfi  45910  inmap  45925  fsumiunss  46291  islptre  46335  sumnnodd  46346  limcresiooub  46356  limcresioolb  46357  limcleqr  46358  limclner  46365  limclr  46369  limsuplesup  46413  limsuppnfdlem  46415  limsupres  46419  liminfgord  46468  liminfgf  46472  liminfcl  46477  limsupresxr  46480  liminfresxr  46481  liminfval2  46482  liminflelimsuplem  46489  liminfvalxr  46497  icccncfext  46601  fourierdlem20  46841  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem76  46896  fourierdlem103  46923  fourierdlem104  46924  fourierdlem113  46933  fouriersw  46945  salgencntex  47057  sge0less  47106  sge0resplit  47120  sge0split  47123  sge0iunmptlemre  47129  sge0fodjrnlem  47130  caragencmpl  47249  ovolval2lem  47357  ovolval2  47358  ovolval3  47361  ovolval4lem2  47364  sssmf  47452  nthrucw  47607  fcoreslem4  47803  fcoresf1  47806  fcoresfo  47808  3f1oss1  47812  rngchomrnghmresALTV  49044  termc  50297