Theorem inss2 4192

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 4163	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4191	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3983	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3902   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  inindif  4329  difin0  4428  iunxdif3  5052  relin2  5770  relres  5972  idssxp  6016  ssrnres  6144  cnvrescnv  6161  ordin  6355  onfr  6364  ordelinel  6428  fnresin2  6626  fresaunres2  6714  ssimaex  6927  exfo  7059  ffvresb  7080  fnfvimad  7190  ofrfvalg  7640  ofval  7643  ofrval  7644  off  7650  ofres  7651  ofco  7657  fnwelem  8083  fnse  8085  fprlem1  8252  tfrlem5  8321  pmresg  8820  ixpfi2  9262  elfiun  9345  marypha1lem  9348  ordtypelem6  9440  ordtypelem7  9441  hartogslem1  9459  unxpwdom  9506  epfrs  9652  tcmin  9660  bnd2  9817  tskwe  9874  r0weon  9934  infxpenlem  9935  djuinf  10111  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem15  10155  ackbij1lem16  10156  ackbij1b  10160  sdom2en01  10224  fin23lem26  10247  fin23lem13  10254  isfin1-3  10308  fin56  10315  fin1a2lem9  10330  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe2lem11  10564  fpwwe2  10566  canthwelem  10573  gruima  10725  ingru  10738  gruina  10741  grur1a  10742  ltrelpi  10812  ltrelnq  10849  nqerf  10853  fzfi  13907  xptrrel  14915  rexanuz  15281  limsupgord  15407  limsupcl  15408  limsupgf  15410  limsupgle  15412  o1of2  15548  o1rlimmul  15554  ackbijnn  15763  bitsinv1  16381  bitsinvp1  16388  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  sadeq  16411  smupval  16427  prmrec  16862  structcnvcnv  17092  ressbasss  17178  ressbasssOLD  17179  ressress  17186  restsspw  17363  submre  17536  isacs1i  17592  rescabs  17769  resscat  17788  funcres2c  17839  ressffth  17876  catccatid  18042  catcisolem  18046  catciso  18047  yoniso  18220  resspos  18364  resstos  18365  acsinfd  18491  acsdomd  18492  tsrss  18524  idresefmnd  18836  idrespermg  19352  mvdco  19386  lsmmod  19616  submomnd  20073  rnghmresfn  20564  rnghmsscmap  20575  rhmresfn  20593  rhmsscmap  20604  rhmsubclem4  20633  acsfn1p  20744  suborng  20821  lssacs  20930  lidlssbas  21180  zringlpirlem2  21430  zringlpirlem3  21431  asplss  21841  ressmplbas  21995  subrgmpl  21999  mplind  22037  ressply1bas  22181  pf1rcl  22305  ressply1evl  22326  evls1addd  22327  evls1muld  22328  evls1vsca  22329  evls1maprhm  22332  ofco2  22407  basdif0  22909  eltg4i  22916  ntrss2  23013  ntrin  23017  isopn3  23022  resttopon  23117  restuni2  23123  restcld  23128  restfpw  23135  neitr  23136  cnrest2r  23243  cnpresti  23244  cnprest  23245  lmss  23254  cnrmi  23316  restcnrm  23318  resthauslem  23319  imacmp  23353  fiuncmp  23360  subislly  23437  islly2  23440  cldllycmp  23451  hauspwdom  23457  kgeni  23493  llycmpkgen2  23506  ptbasfi  23537  ptclsg  23571  ptcnplem  23577  txtube  23596  txcmplem2  23598  txkgen  23608  kqdisj  23688  fbasrn  23840  trfg  23847  isufil2  23864  fmfnfmlem4  23913  hauspwpwf1  23943  txflf  23962  alexsubALTlem4  24006  tmdgsum2  24052  tsmsres  24100  tsmsxplem1  24109  ustexsym  24172  ustund  24178  trust  24185  utoptop  24190  restutop  24193  metrest  24480  restmetu  24526  tgioo  24752  reconnlem2  24784  cphsqrtcl  25152  tcphcph  25205  cfilresi  25263  caussi  25265  causs  25266  ovolfioo  25436  ovolficc  25437  ovolficcss  25438  ovolfsf  25440  ovollb  25448  ovolicc2lem1  25486  ovolicc2lem2  25487  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2  25491  nulmbl  25504  voliunlem1  25519  ovolfs2  25540  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombllem6  25557  uniioombl  25558  dyadmbllem  25568  dyadmbl  25569  opnmbllem  25570  volcn  25575  volivth  25576  mbfadd  25630  mbfsub  25631  i1fima  25647  i1fima2  25648  i1fd  25650  i1fadd  25664  i1fmul  25665  itg1addlem2  25666  itg1addlem4  25668  itg1addlem5  25669  i1fres  25674  mbfmul  25695  bddmulibl  25808  ellimc2  25846  ellimc3  25848  limcflf  25850  limcresi  25854  limciun  25863  dvreslem  25878  dvres2lem  25879  dvres3a  25883  cpnres  25907  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvmptres3  25928  lhop1lem  25986  rlimcnp2  26944  xrlimcnp  26946  chpchtsum  27198  2sqlem8  27405  2sqlem9  27406  rpvmasumlem  27466  rplogsum  27506  dirith2  27507  nosupbnd2  27696  axtgsegcon  28548  axtg5seg  28549  axtgbtwnid  28550  axtgpasch  28551  axtgcont1  28552  tglng  28630  chdmm1i  31565  chm0i  31578  ledii  31624  lejdii  31626  pjoml2i  31673  pjoml4i  31675  cmcmlem  31679  cmbr4i  31689  osumcori  31731  pjssmii  31769  mayete3i  31816  riesz4  32152  riesz1  32153  cnlnadjeu  32166  nmopadjlei  32176  pjclem1  32283  pjci  32288  mdbr3  32385  mdbr4  32386  dmdbr2  32391  dmdbr5  32396  ssmd2  32400  mdslj1i  32407  mdslj2i  32408  mdsl1i  32409  mdsl2bi  32411  mdslmd1lem1  32413  mdslmd1lem2  32414  mdslmd2i  32418  csmdsymi  32422  cvexchlem  32456  atomli  32470  atcvat4i  32485  difininv  32604  disjxpin  32675  imadifxp  32688  off2  32731  mptiffisupp  32783  indsumin  32954  indf1ofs  32959  idlinsubrg  33524  ressply1invg  33662  evls1subd  33665  algextdeglem7  33901  algextdeglem8  33902  ordtrestNEW  34099  pnfneige0  34129  lmxrge0  34130  qqhnm  34168  qqhcn  34169  rrhre  34199  gsumesum  34237  esumlub  34238  esumcst  34241  esumpcvgval  34256  hasheuni  34263  esumcvg  34264  sigainb  34314  carsgclctunlem2  34497  sibfinima  34517  sibfof  34518  eulerpartlemelr  34535  eulerpartlemgh  34556  eulerpartlemgf  34557  eulerpartlemgs2  34558  eulerpartlemn  34559  probmeasb  34608  cndprob01  34613  hashreprin  34798  reprfi2  34801  breprexpnat  34812  hgt750lemd  34826  hgt750lema  34835  tgoldbachgtde  34838  tgoldbachgtda  34839  tgoldbachgt  34841  bnj1293  34992  connpconn  35451  iccllysconn  35466  cvmsss2  35490  cvmcov2  35491  cvmopnlem  35494  cvmliftmolem2  35498  cvmlift2lem12  35530  mvrsfpw  35722  elmsta  35764  msubvrs  35776  mclsind  35786  nepss  35934  dfon2lem4  36000  trer  36532  neiin  36548  neibastop1  36575  neibastop2lem  36576  topmeet  36580  filnetlem3  36596  weiunfr  36683  bj-disj2r  37276  bj-restpw  37345  bj-restb  37347  bj-restuni2  37351  bj-ablsscmn  37533  topdifinffinlem  37602  opnmbllem0  37907  mblfinlem4  37911  mbfposadd  37918  heibor1lem  38060  heiborlem1  38062  heiborlem3  38064  heiborlem10  38071  opidonOLD  38103  disjimin  39102  lshpinN  39365  lcvexchlem1  39410  lcvexchlem5  39414  pmod1i  40224  pmodN  40226  osumcllem7N  40338  pexmidlem4N  40349  dochdmj1  41766  dochexmidlem4  41839  lcfrlem25  41943  mapd1o  42024  mapdin  42038  elrfi  43051  elrfirn  43052  fnwe2lem2  43408  aomclem2  43412  lsmfgcl  43431  lmhmfgima  43441  lmhmfgsplit  43443  lmhmlnmsplit  43444  hbt  43487  ofoafg  43711  trrelind  44021  iunrelexp0  44058  isotone2  44405  grumnudlem  44641  ismnushort  44657  onfrALTlem3  44900  onfrALTlem2  44902  onfrALTlem3VD  45242  onfrALTlem2VD  45244  iunconnlem2  45290  wfac8prim  45358  restuni6  45481  disjinfi  45551  inmap  45567  fsumiunss  45935  islptre  45979  sumnnodd  45990  limcresiooub  46000  limcresioolb  46001  limcleqr  46002  limclner  46009  limclr  46013  limsuplesup  46057  limsuppnfdlem  46059  limsupres  46063  liminfgord  46112  liminfgf  46116  liminfcl  46121  limsupresxr  46124  liminfresxr  46125  liminfval2  46126  liminflelimsuplem  46133  liminfvalxr  46141  icccncfext  46245  fourierdlem20  46485  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem76  46540  fourierdlem103  46567  fourierdlem104  46568  fourierdlem113  46577  fouriersw  46589  salgencntex  46701  sge0less  46750  sge0resplit  46764  sge0split  46767  sge0iunmptlemre  46773  sge0fodjrnlem  46774  caragencmpl  46893  ovolval2lem  47001  ovolval2  47002  ovolval3  47005  ovolval4lem2  47008  sssmf  47096  nthrucw  47244  fcoreslem4  47426  fcoresf1  47429  fcoresfo  47431  3f1oss1  47435  rngchomrnghmresALTV  48639  termc  49878