Theorem inss2 4191

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 4190	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3985	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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912  df-ss 3922

This theorem is referenced by:  inindif  4328  difin0  4427  iunxdif3  5047  relin2  5760  relres  5960  idssxp  6004  ssrnres  6131  cnvrescnv  6148  ordin  6341  onfr  6350  ordelinel  6414  fnresin2  6612  fresaunres2  6700  ssimaex  6912  exfo  7043  ffvresb  7063  fnfvimad  7174  ofrfvalg  7625  ofval  7628  ofrval  7629  off  7635  ofres  7636  ofco  7642  fnwelem  8071  fnse  8073  fprlem1  8240  tfrlem5  8309  pmresg  8804  ixpfi2  9259  elfiun  9339  marypha1lem  9342  ordtypelem6  9434  ordtypelem7  9435  hartogslem1  9453  unxpwdom  9500  epfrs  9646  tcmin  9656  bnd2  9808  tskwe  9865  r0weon  9925  infxpenlem  9926  djuinf  10102  ackbij1lem9  10140  ackbij1lem10  10141  ackbij1lem15  10146  ackbij1lem16  10147  ackbij1b  10151  sdom2en01  10215  fin23lem26  10238  fin23lem13  10245  isfin1-3  10299  fin56  10306  fin1a2lem9  10321  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe2lem11  10554  fpwwe2  10556  canthwelem  10563  gruima  10715  ingru  10728  gruina  10731  grur1a  10732  ltrelpi  10802  ltrelnq  10839  nqerf  10843  fzfi  13898  xptrrel  14906  rexanuz  15272  limsupgord  15398  limsupcl  15399  limsupgf  15401  limsupgle  15403  o1of2  15539  o1rlimmul  15545  ackbijnn  15754  bitsinv1  16372  bitsinvp1  16379  sadcaddlem  16387  sadadd2lem  16389  sadadd3  16391  sadaddlem  16396  sadasslem  16400  sadeq  16402  smupval  16418  prmrec  16853  structcnvcnv  17083  ressbasss  17169  ressbasssOLD  17170  ressress  17177  restsspw  17354  submre  17526  isacs1i  17582  rescabs  17759  resscat  17778  funcres2c  17829  ressffth  17866  catccatid  18032  catcisolem  18036  catciso  18037  yoniso  18210  resspos  18354  resstos  18355  acsinfd  18481  acsdomd  18482  tsrss  18514  idresefmnd  18792  idrespermg  19309  mvdco  19343  lsmmod  19573  submomnd  20030  rnghmresfn  20523  rnghmsscmap  20534  rhmresfn  20552  rhmsscmap  20563  rhmsubclem4  20592  acsfn1p  20703  suborng  20780  lssacs  20889  lidlssbas  21139  zringlpirlem2  21389  zringlpirlem3  21390  asplss  21800  ressmplbas  21952  subrgmpl  21956  mplind  21994  ressply1bas  22130  pf1rcl  22253  ressply1evl  22274  evls1addd  22275  evls1muld  22276  evls1vsca  22277  evls1maprhm  22280  ofco2  22355  basdif0  22857  eltg4i  22864  ntrss2  22961  ntrin  22965  isopn3  22970  resttopon  23065  restuni2  23071  restcld  23076  restfpw  23083  neitr  23084  cnrest2r  23191  cnpresti  23192  cnprest  23193  lmss  23202  cnrmi  23264  restcnrm  23266  resthauslem  23267  imacmp  23301  fiuncmp  23308  subislly  23385  islly2  23388  cldllycmp  23399  hauspwdom  23405  kgeni  23441  llycmpkgen2  23454  ptbasfi  23485  ptclsg  23519  ptcnplem  23525  txtube  23544  txcmplem2  23546  txkgen  23556  kqdisj  23636  fbasrn  23788  trfg  23795  isufil2  23812  fmfnfmlem4  23861  hauspwpwf1  23891  txflf  23910  alexsubALTlem4  23954  tmdgsum2  24000  tsmsres  24048  tsmsxplem1  24057  ustexsym  24120  ustund  24126  trust  24134  utoptop  24139  restutop  24142  metrest  24429  restmetu  24475  tgioo  24701  reconnlem2  24733  cphsqrtcl  25101  tcphcph  25154  cfilresi  25212  caussi  25214  causs  25215  ovolfioo  25385  ovolficc  25386  ovolficcss  25387  ovolfsf  25389  ovollb  25397  ovolicc2lem1  25435  ovolicc2lem2  25436  ovolicc2lem3  25437  ovolicc2lem4  25438  ovolicc2  25440  nulmbl  25453  voliunlem1  25468  ovolfs2  25489  uniiccdif  25496  uniioovol  25497  uniiccvol  25498  uniioombllem2  25501  uniioombllem3a  25502  uniioombllem3  25503  uniioombllem4  25504  uniioombllem5  25505  uniioombllem6  25506  uniioombl  25507  dyadmbllem  25517  dyadmbl  25518  opnmbllem  25519  volcn  25524  volivth  25525  mbfadd  25579  mbfsub  25580  i1fima  25596  i1fima2  25597  i1fd  25599  i1fadd  25613  i1fmul  25614  itg1addlem2  25615  itg1addlem4  25617  itg1addlem5  25618  i1fres  25623  mbfmul  25644  bddmulibl  25757  ellimc2  25795  ellimc3  25797  limcflf  25799  limcresi  25803  limciun  25812  dvreslem  25827  dvres2lem  25828  dvres3a  25832  cpnres  25856  dvaddbr  25857  dvmulbr  25858  dvmulbrOLD  25859  dvmptres3  25877  lhop1lem  25935  rlimcnp2  26893  xrlimcnp  26895  chpchtsum  27147  2sqlem8  27354  2sqlem9  27355  rpvmasumlem  27415  rplogsum  27455  dirith2  27456  nosupbnd2  27645  axtgsegcon  28428  axtg5seg  28429  axtgbtwnid  28430  axtgpasch  28431  axtgcont1  28432  tglng  28510  chdmm1i  31440  chm0i  31453  ledii  31499  lejdii  31501  pjoml2i  31548  pjoml4i  31550  cmcmlem  31554  cmbr4i  31564  osumcori  31606  pjssmii  31644  mayete3i  31691  riesz4  32027  riesz1  32028  cnlnadjeu  32041  nmopadjlei  32051  pjclem1  32158  pjci  32163  mdbr3  32260  mdbr4  32261  dmdbr2  32266  dmdbr5  32271  ssmd2  32275  mdslj1i  32282  mdslj2i  32283  mdsl1i  32284  mdsl2bi  32286  mdslmd1lem1  32288  mdslmd1lem2  32289  mdslmd2i  32293  csmdsymi  32297  cvexchlem  32331  atomli  32345  atcvat4i  32360  difininv  32480  disjxpin  32551  imadifxp  32564  off2  32603  mptiffisupp  32654  indsumin  32824  indf1ofs  32828  idlinsubrg  33387  ressply1invg  33523  evls1subd  33526  algextdeglem7  33709  algextdeglem8  33710  ordtrestNEW  33907  pnfneige0  33937  lmxrge0  33938  qqhnm  33976  qqhcn  33977  rrhre  34007  gsumesum  34045  esumlub  34046  esumcst  34049  esumpcvgval  34064  hasheuni  34071  esumcvg  34072  sigainb  34122  carsgclctunlem2  34306  sibfinima  34326  sibfof  34327  eulerpartlemelr  34344  eulerpartlemgh  34365  eulerpartlemgf  34366  eulerpartlemgs2  34367  eulerpartlemn  34368  probmeasb  34417  cndprob01  34422  hashreprin  34607  reprfi2  34610  breprexpnat  34621  hgt750lemd  34635  hgt750lema  34644  tgoldbachgtde  34647  tgoldbachgtda  34648  tgoldbachgt  34650  bnj1293  34802  connpconn  35227  iccllysconn  35242  cvmsss2  35266  cvmcov2  35267  cvmopnlem  35270  cvmliftmolem2  35274  cvmlift2lem12  35306  mvrsfpw  35498  elmsta  35540  msubvrs  35552  mclsind  35562  nepss  35710  dfon2lem4  35779  trer  36309  neiin  36325  neibastop1  36352  neibastop2lem  36353  topmeet  36357  filnetlem3  36373  weiunfr  36460  bj-disj2r  37021  bj-restpw  37085  bj-restb  37087  bj-restuni2  37091  bj-ablsscmn  37271  topdifinffinlem  37340  opnmbllem0  37655  mblfinlem4  37659  mbfposadd  37666  heibor1lem  37808  heiborlem1  37810  heiborlem3  37812  heiborlem10  37819  opidonOLD  37851  disjimin  38748  lshpinN  38987  lcvexchlem1  39032  lcvexchlem5  39036  pmod1i  39847  pmodN  39849  osumcllem7N  39961  pexmidlem4N  39972  dochdmj1  41389  dochexmidlem4  41462  lcfrlem25  41566  mapd1o  41647  mapdin  41661  elrfi  42687  elrfirn  42688  fnwe2lem2  43044  aomclem2  43048  lsmfgcl  43067  lmhmfgima  43077  lmhmfgsplit  43079  lmhmlnmsplit  43080  hbt  43123  ofoafg  43347  trrelind  43658  iunrelexp0  43695  isotone2  44042  grumnudlem  44278  ismnushort  44294  onfrALTlem3  44538  onfrALTlem2  44540  onfrALTlem3VD  44880  onfrALTlem2VD  44882  iunconnlem2  44928  wfac8prim  44996  restuni6  45120  disjinfi  45190  inmap  45207  fsumiunss  45576  islptre  45620  sumnnodd  45631  limcresiooub  45643  limcresioolb  45644  limcleqr  45645  limclner  45652  limclr  45656  limsuplesup  45700  limsuppnfdlem  45702  limsupres  45706  liminfgord  45755  liminfgf  45759  liminfcl  45764  limsupresxr  45767  liminfresxr  45768  liminfval2  45769  liminflelimsuplem  45776  liminfvalxr  45784  icccncfext  45888  fourierdlem20  46128  fourierdlem48  46155  fourierdlem49  46156  fourierdlem50  46157  fourierdlem76  46183  fourierdlem103  46210  fourierdlem104  46211  fourierdlem113  46220  fouriersw  46232  salgencntex  46344  sge0less  46393  sge0resplit  46407  sge0split  46410  sge0iunmptlemre  46416  sge0fodjrnlem  46417  caragencmpl  46536  ovolval2lem  46644  ovolval2  46645  ovolval3  46648  ovolval4lem2  46651  sssmf  46739  fcoreslem4  47070  fcoresf1  47073  fcoresfo  47075  3f1oss1  47079  rngchomrnghmresALTV  48283  termc  49524