Theorem inss2 4230

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 4202	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4229	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 4018	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3948   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3956  df-ss 3966

This theorem is referenced by:  difin0  4474  iunxdif3  5099  relin2  5814  relres  6011  idssxp  6049  ssrnres  6178  cnvrescnv  6195  ordin  6395  onfr  6404  ordelinel  6466  fnresin2  6677  fresaunres2  6764  ssimaex  6977  exfo  7107  ffvresb  7127  fnfvimad  7239  ofrfvalg  7682  ofval  7685  ofrval  7686  off  7692  ofres  7693  ofco  7697  fnwelem  8121  fnse  8123  fprlem1  8289  tfrlem5  8384  pmresg  8868  nnfiOLD  9236  ixpfi2  9354  elfiun  9429  marypha1lem  9432  ordtypelem6  9522  ordtypelem7  9523  hartogslem1  9541  unxpwdom  9588  epfrs  9730  tcmin  9740  bnd2  9892  tskwe  9949  r0weon  10011  infxpenlem  10012  djuinf  10187  ackbij1lem9  10227  ackbij1lem10  10228  ackbij1lem15  10233  ackbij1lem16  10234  ackbij1b  10238  sdom2en01  10301  fin23lem26  10324  fin23lem13  10331  isfin1-3  10385  fin56  10392  fin1a2lem9  10407  brdom3  10527  brdom5  10528  brdom4  10529  fpwwe2lem11  10640  fpwwe2  10642  canthwelem  10649  gruima  10801  ingru  10814  gruina  10817  grur1a  10818  ltrelpi  10888  ltrelnq  10925  nqerf  10929  fzfi  13943  xptrrel  14933  rexanuz  15298  limsupgord  15422  limsupcl  15423  limsupgf  15425  limsupgle  15427  o1of2  15563  o1rlimmul  15569  ackbijnn  15780  bitsinv1  16389  bitsinvp1  16396  sadcaddlem  16404  sadadd2lem  16406  sadadd3  16408  sadaddlem  16413  sadasslem  16417  sadeq  16419  smupval  16435  prmrec  16861  structcnvcnv  17092  ressbasss  17189  ressbasssOLD  17190  ressress  17199  restsspw  17383  submre  17555  isacs1i  17607  rescabs  17788  rescabsOLD  17789  resscat  17808  funcres2c  17858  ressffth  17895  catccatid  18062  catcisolem  18066  catciso  18067  yoniso  18244  acsinfd  18515  acsdomd  18516  tsrss  18548  idresefmnd  18818  idrespermg  19322  mvdco  19356  lsmmod  19586  acsfn1p  20560  lssacs  20724  lidlssbas  20981  zringlpirlem2  21236  zringlpirlem3  21237  asplss  21649  ressmplbas  21804  subrgmpl  21808  mplind  21852  ressply1bas  21973  pf1rcl  22090  ofco2  22175  basdif0  22678  eltg4i  22685  ntrss2  22783  ntrin  22787  isopn3  22792  resttopon  22887  restuni2  22893  restcld  22898  restfpw  22905  neitr  22906  cnrest2r  23013  cnpresti  23014  cnprest  23015  lmss  23024  cnrmi  23086  restcnrm  23088  resthauslem  23089  imacmp  23123  fiuncmp  23130  subislly  23207  islly2  23210  cldllycmp  23221  hauspwdom  23227  kgeni  23263  llycmpkgen2  23276  ptbasfi  23307  ptclsg  23341  ptcnplem  23347  txtube  23366  txcmplem2  23368  txkgen  23378  kqdisj  23458  fbasrn  23610  trfg  23617  isufil2  23634  fmfnfmlem4  23683  hauspwpwf1  23713  txflf  23732  alexsubALTlem4  23776  tmdgsum2  23822  tsmsres  23870  tsmsxplem1  23879  ustexsym  23942  ustund  23948  trust  23956  utoptop  23961  restutop  23964  metrest  24255  restmetu  24301  tgioo  24534  reconnlem2  24565  cphsqrtcl  24934  tcphcph  24987  cfilresi  25045  caussi  25047  causs  25048  ovolfioo  25218  ovolficc  25219  ovolficcss  25220  ovolfsf  25222  ovollb  25230  ovolicc2lem1  25268  ovolicc2lem2  25269  ovolicc2lem3  25270  ovolicc2lem4  25271  ovolicc2  25273  nulmbl  25286  voliunlem1  25301  ovolfs2  25322  uniiccdif  25329  uniioovol  25330  uniiccvol  25331  uniioombllem2  25334  uniioombllem3a  25335  uniioombllem3  25336  uniioombllem4  25337  uniioombllem5  25338  uniioombllem6  25339  uniioombl  25340  dyadmbllem  25350  dyadmbl  25351  opnmbllem  25352  volcn  25357  volivth  25358  mbfadd  25412  mbfsub  25413  i1fima  25429  i1fima2  25430  i1fd  25432  i1fadd  25446  i1fmul  25447  itg1addlem2  25448  itg1addlem4  25450  itg1addlem4OLD  25451  itg1addlem5  25452  i1fres  25457  mbfmul  25478  bddmulibl  25590  ellimc2  25628  ellimc3  25630  limcflf  25632  limcresi  25636  limciun  25645  dvreslem  25660  dvres2lem  25661  dvres3a  25665  cpnres  25688  dvaddbr  25689  dvmulbr  25690  dvmptres3  25707  lhop1lem  25764  rlimcnp2  26705  xrlimcnp  26707  chpchtsum  26956  2sqlem8  27163  2sqlem9  27164  rpvmasumlem  27224  rplogsum  27264  dirith2  27265  nosupbnd2  27453  axtgsegcon  27980  axtg5seg  27981  axtgbtwnid  27982  axtgpasch  27983  axtgcont1  27984  tglng  28062  chdmm1i  30995  chm0i  31008  ledii  31054  lejdii  31056  pjoml2i  31103  pjoml4i  31105  cmcmlem  31109  cmbr4i  31119  osumcori  31161  pjssmii  31199  mayete3i  31246  riesz4  31582  riesz1  31583  cnlnadjeu  31596  nmopadjlei  31606  pjclem1  31713  pjci  31718  mdbr3  31815  mdbr4  31816  dmdbr2  31821  dmdbr5  31826  ssmd2  31830  mdslj1i  31837  mdslj2i  31838  mdsl1i  31839  mdsl2bi  31841  mdslmd1lem1  31843  mdslmd1lem2  31844  mdslmd2i  31848  csmdsymi  31852  cvexchlem  31886  atomli  31900  atcvat4i  31915  inindif  32019  difininv  32020  disjxpin  32084  imadifxp  32097  off2  32131  mptiffisupp  32180  resspos  32401  resstos  32402  submomnd  32496  suborng  32701  idlinsubrg  32821  ressply1evl  32919  evls1addd  32920  evls1muld  32921  evls1vsca  32922  ressply1invg  32930  evls1maprhm  33046  algextdeglem7  33066  algextdeglem8  33067  ordtrestNEW  33197  pnfneige0  33227  lmxrge0  33228  qqhnm  33266  qqhcn  33267  rrhre  33297  indsumin  33316  indf1ofs  33320  gsumesum  33353  esumlub  33354  esumcst  33357  esumpcvgval  33372  hasheuni  33379  esumcvg  33380  sigainb  33430  carsgclctunlem2  33614  sibfinima  33634  sibfof  33635  eulerpartlemelr  33652  eulerpartlemgh  33673  eulerpartlemgf  33674  eulerpartlemgs2  33675  eulerpartlemn  33676  probmeasb  33725  cndprob01  33730  hashreprin  33928  reprfi2  33931  breprexpnat  33942  hgt750lemd  33956  hgt750lema  33965  tgoldbachgtde  33968  tgoldbachgtda  33969  tgoldbachgt  33971  bnj1293  34123  connpconn  34522  iccllysconn  34537  cvmsss2  34561  cvmcov2  34562  cvmopnlem  34565  cvmliftmolem2  34569  cvmlift2lem12  34601  mvrsfpw  34793  elmsta  34835  msubvrs  34847  mclsind  34857  nepss  34989  dfon2lem4  35060  gg-dvmulbr  35463  trer  35506  neiin  35522  neibastop1  35549  neibastop2lem  35550  topmeet  35554  filnetlem3  35570  bj-disj2r  36214  bj-restpw  36278  bj-restb  36280  bj-restuni2  36284  bj-ablsscmn  36464  topdifinffinlem  36533  opnmbllem0  36829  mblfinlem4  36833  mbfposadd  36840  heibor1lem  36982  heiborlem1  36984  heiborlem3  36986  heiborlem10  36993  opidonOLD  37025  disjimin  37926  lshpinN  38164  lcvexchlem1  38209  lcvexchlem5  38213  pmod1i  39024  pmodN  39026  osumcllem7N  39138  pexmidlem4N  39149  dochdmj1  40566  dochexmidlem4  40639  lcfrlem25  40743  mapd1o  40824  mapdin  40838  elrfi  41736  elrfirn  41737  fnwe2lem2  42097  aomclem2  42101  lsmfgcl  42120  lmhmfgima  42130  lmhmfgsplit  42132  lmhmlnmsplit  42133  hbt  42176  ofoafg  42408  trrelind  42720  iunrelexp0  42757  isotone2  43104  grumnudlem  43348  ismnushort  43364  onfrALTlem3  43609  onfrALTlem2  43611  onfrALTlem3VD  43952  onfrALTlem2VD  43954  iunconnlem2  44000  restuni6  44114  disjinfi  44191  inmap  44208  dmresss  44233  fsumiunss  44591  islptre  44635  sumnnodd  44646  limcresiooub  44658  limcresioolb  44659  limcleqr  44660  limclner  44667  limclr  44671  limsuplesup  44715  limsuppnfdlem  44717  limsupres  44721  liminfgord  44770  liminfgf  44774  liminfcl  44779  limsupresxr  44782  liminfresxr  44783  liminfval2  44784  liminflelimsuplem  44791  liminfvalxr  44799  icccncfext  44903  fourierdlem20  45143  fourierdlem48  45170  fourierdlem49  45171  fourierdlem50  45172  fourierdlem76  45198  fourierdlem103  45225  fourierdlem104  45226  fourierdlem113  45235  fouriersw  45247  salgencntex  45359  sge0less  45408  sge0resplit  45422  sge0split  45425  sge0iunmptlemre  45431  sge0fodjrnlem  45432  caragencmpl  45551  ovolval2lem  45659  ovolval2  45660  ovolval3  45663  ovolval4lem2  45666  sssmf  45754  fcoreslem4  46076  fcoresf1  46079  fcoresfo  46081  rnghmresfn  46951  rnghmsscmap  46962  rngchomrnghmresALTV  46984  rhmresfn  46997  rhmsscmap  47008  rhmsubclem4  47077