Theorem inss2 4187

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 4159	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4186	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3981	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-in 3909  df-ss 3919

This theorem is referenced by:  inindif  4325  difin0  4425  uniin  4886  iunxdif3  5049  relin2  5782  relres  5987  idssxp  6034  rnin  6126  ssrnres  6159  cnvrescnv  6177  ordin  6371  onfr  6380  ordelinel  6444  fnresin2  6642  fresaunres2  6731  ssimaex  6947  exfo  7081  ffvresb  7102  fnfvimad  7213  ofrfvalg  7663  ofval  7666  ofrval  7667  off  7673  ofres  7674  ofco  7680  fnwelem  8105  fnse  8107  fprlem1  8275  tfrlem5  8344  pmresg  8846  ixpfi2  9287  elfiun  9370  marypha1lem  9373  ordtypelem6  9465  ordtypelem7  9466  hartogslem1  9484  unxpwdom  9531  epfrs  9680  tcmin  9688  bnd2  9845  tskwe  9902  r0weon  9962  infxpenlem  9963  djuinf  10139  ackbij1lem9  10177  ackbij1lem10  10178  ackbij1lem15  10183  ackbij1lem16  10184  ackbij1b  10188  sdom2en01  10253  fin23lem26  10276  fin23lem13  10283  isfin1-3  10337  fin56  10344  fin1a2lem9  10359  brdom3  10479  brdom5  10480  brdom4  10481  fpwwe2lem11  10593  fpwwe2  10595  canthwelem  10602  gruima  10754  ingru  10767  gruina  10770  grur1a  10771  ltrelpi  10841  ltrelnq  10878  nqerf  10882  fzfi  13979  xptrrel  14987  rexanuz  15364  limsupgord  15490  limsupcl  15491  limsupgf  15493  limsupgle  15495  o1of2  15631  o1rlimmul  15637  ackbijnn  15849  bitsinv1  16467  bitsinvp1  16474  sadcaddlem  16482  sadadd2lem  16484  sadadd3  16486  sadaddlem  16491  sadasslem  16495  sadeq  16497  smupval  16513  prmrec  16949  structcnvcnv  17180  ressbasss  17266  ressbasssOLD  17267  ressress  17274  restsspw  17451  submre  17624  isacs1i  17680  rescabs  17857  resscat  17876  funcres2c  17927  ressffth  17964  catccatid  18130  catcisolem  18134  catciso  18135  yoniso  18308  resspos  18452  resstos  18453  acsinfd  18579  acsdomd  18580  tsrss  18612  idresefmnd  18924  idrespermg  19442  mvdco  19476  lsmmod  19706  submomnd  20163  rnghmresfn  20656  rnghmsscmap  20667  rhmresfn  20685  rhmsscmap  20696  rhmsubclem4  20725  acsfn1p  20836  suborng  20913  lssacs  21022  lidlssbas  21271  zringlpirlem2  21503  zringlpirlem3  21504  asplss  21913  ressmplbas  22068  subrgmpl  22072  mplind  22111  ressply1bas  22278  pf1rcl  22400  ressply1evl  22421  evls1addd  22422  evls1muld  22423  evls1vsca  22424  evls1maprhm  22427  ofco2  22499  basdif0  23001  eltg4i  23008  ntrss2  23105  ntrin  23109  isopn3  23114  resttopon  23209  restuni2  23215  restcld  23220  restfpw  23227  neitr  23228  cnrest2r  23335  cnpresti  23336  cnprest  23337  lmss  23346  cnrmi  23408  restcnrm  23410  resthauslem  23411  imacmp  23445  fiuncmp  23452  subislly  23529  islly2  23532  cldllycmp  23543  hauspwdom  23549  kgeni  23585  llycmpkgen2  23598  ptbasfi  23629  ptclsg  23663  ptcnplem  23669  txtube  23688  txcmplem2  23690  txkgen  23700  kqdisj  23780  fbasrn  23932  trfg  23939  isufil2  23956  fmfnfmlem4  24005  hauspwpwf1  24035  txflf  24054  alexsubALTlem4  24098  tmdgsum2  24144  tsmsres  24192  tsmsxplem1  24201  ustexsym  24264  ustund  24270  trust  24277  utoptop  24282  restutop  24285  metrest  24572  restmetu  24618  tgioo  24844  reconnlem2  24876  cphsqrtcl  25234  tcphcph  25287  cfilresi  25345  caussi  25347  causs  25348  ovolfioo  25517  ovolficc  25518  ovolficcss  25519  ovolfsf  25521  ovollb  25529  ovolicc2lem1  25567  ovolicc2lem2  25568  ovolicc2lem3  25569  ovolicc2lem4  25570  ovolicc2  25572  nulmbl  25585  voliunlem1  25600  ovolfs2  25621  uniiccdif  25628  uniioovol  25629  uniiccvol  25630  uniioombllem2  25633  uniioombllem3a  25634  uniioombllem3  25635  uniioombllem4  25636  uniioombllem5  25637  uniioombllem6  25638  uniioombl  25639  dyadmbllem  25649  dyadmbl  25650  opnmbllem  25651  volcn  25656  volivth  25657  mbfadd  25711  mbfsub  25712  i1fima  25728  i1fima2  25729  i1fd  25731  i1fadd  25745  i1fmul  25746  itg1addlem2  25747  itg1addlem4  25749  itg1addlem5  25750  i1fres  25755  mbfmul  25776  bddmulibl  25889  ellimc2  25927  ellimc3  25929  limcflf  25931  limcresi  25935  limciun  25944  dvreslem  25959  dvres2lem  25960  dvres3a  25964  cpnres  25987  dvaddbr  25988  dvmulbr  25989  dvmptres3  26006  lhop1lem  26063  rlimcnp2  27019  xrlimcnp  27021  chpchtsum  27271  2sqlem8  27478  2sqlem9  27479  rpvmasumlem  27539  rplogsum  27579  dirith2  27580  nosupbnd2  27768  axtgsegcon  28621  axtg5seg  28622  axtgbtwnid  28623  axtgpasch  28624  axtgcont1  28625  tglng  28703  chdmm1i  31637  chm0i  31650  ledii  31696  lejdii  31698  pjoml2i  31745  pjoml4i  31747  cmcmlem  31751  cmbr4i  31761  osumcori  31803  pjssmii  31841  mayete3i  31888  riesz4  32224  riesz1  32225  cnlnadjeu  32238  nmopadjlei  32248  pjclem1  32355  pjci  32360  mdbr3  32457  mdbr4  32458  dmdbr2  32463  dmdbr5  32468  ssmd2  32472  mdslj1i  32479  mdslj2i  32480  mdsl1i  32481  mdsl2bi  32483  mdslmd1lem1  32485  mdslmd1lem2  32486  mdslmd2i  32490  csmdsymi  32494  cvexchlem  32528  atomli  32542  atcvat4i  32557  difininv  32676  disjxpin  32748  imadifxp  32761  off2  32804  mptiffisupp  32856  indsumin  33000  indf1ofs  33005  idlinsubrg  33578  ressply1invg  33726  evls1subd  33729  algextdeglem7  33981  algextdeglem8  33982  ordtrestNEW  34179  pnfneige0  34209  lmxrge0  34210  qqhnm  34248  qqhcn  34249  rrhre  34279  gsumesum  34317  esumlub  34318  esumcst  34321  esumpcvgval  34336  hasheuni  34343  esumcvg  34344  sigainb  34394  carsgclctunlem2  34577  sibfinima  34597  sibfof  34598  eulerpartlemelr  34615  eulerpartlemgh  34636  eulerpartlemgf  34637  eulerpartlemgs2  34638  eulerpartlemn  34639  probmeasb  34688  cndprob01  34693  hashreprin  34875  reprfi2  34878  breprexpnat  34889  hgt750lemd  34903  hgt750lema  34912  tgoldbachgtde  34915  tgoldbachgtda  34916  tgoldbachgt  34918  bnj1293  35072  connpconn  35546  iccllysconn  35561  cvmsss2  35585  cvmcov2  35586  cvmopnlem  35589  cvmliftmolem2  35593  cvmlift2lem12  35625  mvrsfpw  35817  elmsta  35859  msubvrs  35871  mclsind  35881  nepss  36029  dfon2lem4  36095  trer  36637  neiin  36653  neibastop1  36680  neibastop2lem  36681  topmeet  36685  filnetlem3  36701  weiunfr  36788  elttcirr  36852  bj-disj2r  37474  bj-restpw  37543  bj-restb  37545  bj-restuni2  37549  bj-ablsscmn  37731  topdifinffinlem  37802  opnmbllem0  38116  mblfinlem4  38120  mbfposadd  38127  heibor1lem  38269  heiborlem1  38271  heiborlem3  38273  heiborlem10  38280  opidonOLD  38312  disjimin  39311  lshpinN  39574  lcvexchlem1  39619  lcvexchlem5  39623  pmod1i  40433  pmodN  40435  osumcllem7N  40547  pexmidlem4N  40558  dochdmj1  41975  dochexmidlem4  42048  lcfrlem25  42152  mapd1o  42233  mapdin  42247  elrfi  43236  elrfirn  43237  fnwe2lem2  43589  aomclem2  43593  lsmfgcl  43612  lmhmfgima  43622  lmhmfgsplit  43624  lmhmlnmsplit  43625  hbt  43668  ofoafg  43892  trrelind  44202  iunrelexp0  44239  isotone2  44586  grumnudlem  44822  ismnushort  44838  onfrALTlem3  45081  onfrALTlem2  45083  onfrALTlem3VD  45423  onfrALTlem2VD  45425  iunconnlem2  45471  wfac8prim  45539  restuni6  45661  disjinfi  45731  inmap  45746  fsumiunss  46112  islptre  46156  sumnnodd  46167  limcresiooub  46177  limcresioolb  46178  limcleqr  46179  limclner  46186  limclr  46190  limsuplesup  46234  limsuppnfdlem  46236  limsupres  46240  liminfgord  46289  liminfgf  46293  liminfcl  46298  limsupresxr  46301  liminfresxr  46302  liminfval2  46303  liminflelimsuplem  46310  liminfvalxr  46318  icccncfext  46422  fourierdlem20  46662  fourierdlem48  46689  fourierdlem49  46690  fourierdlem50  46691  fourierdlem76  46717  fourierdlem103  46744  fourierdlem104  46745  fourierdlem113  46754  fouriersw  46766  salgencntex  46878  sge0less  46927  sge0resplit  46941  sge0split  46944  sge0iunmptlemre  46950  sge0fodjrnlem  46951  caragencmpl  47070  ovolval2lem  47178  ovolval2  47179  ovolval3  47182  ovolval4lem2  47185  sssmf  47273  nthrucw  47423  fcoreslem4  47621  fcoresf1  47624  fcoresfo  47626  3f1oss1  47630  rngchomrnghmresALTV  48862  termc  50101