Theorem inss2 4201

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 4172	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4200	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3994	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3913   ⊆ wss 3914

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 3406  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  inindif  4338  difin0  4437  iunxdif3  5059  relin2  5776  relres  5976  idssxp  6020  ssrnres  6151  cnvrescnv  6168  ordin  6362  onfr  6371  ordelinel  6435  fnresin2  6644  fresaunres2  6732  ssimaex  6946  exfo  7077  ffvresb  7097  fnfvimad  7208  ofrfvalg  7661  ofval  7664  ofrval  7665  off  7671  ofres  7672  ofco  7678  fnwelem  8110  fnse  8112  fprlem1  8279  tfrlem5  8348  pmresg  8843  ixpfi2  9301  elfiun  9381  marypha1lem  9384  ordtypelem6  9476  ordtypelem7  9477  hartogslem1  9495  unxpwdom  9542  epfrs  9684  tcmin  9694  bnd2  9846  tskwe  9903  r0weon  9965  infxpenlem  9966  djuinf  10142  ackbij1lem9  10180  ackbij1lem10  10181  ackbij1lem15  10186  ackbij1lem16  10187  ackbij1b  10191  sdom2en01  10255  fin23lem26  10278  fin23lem13  10285  isfin1-3  10339  fin56  10346  fin1a2lem9  10361  brdom3  10481  brdom5  10482  brdom4  10483  fpwwe2lem11  10594  fpwwe2  10596  canthwelem  10603  gruima  10755  ingru  10768  gruina  10771  grur1a  10772  ltrelpi  10842  ltrelnq  10879  nqerf  10883  fzfi  13937  xptrrel  14946  rexanuz  15312  limsupgord  15438  limsupcl  15439  limsupgf  15441  limsupgle  15443  o1of2  15579  o1rlimmul  15585  ackbijnn  15794  bitsinv1  16412  bitsinvp1  16419  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  sadeq  16442  smupval  16458  prmrec  16893  structcnvcnv  17123  ressbasss  17209  ressbasssOLD  17210  ressress  17217  restsspw  17394  submre  17566  isacs1i  17618  rescabs  17795  resscat  17814  funcres2c  17865  ressffth  17902  catccatid  18068  catcisolem  18072  catciso  18073  yoniso  18246  acsinfd  18515  acsdomd  18516  tsrss  18548  idresefmnd  18826  idrespermg  19341  mvdco  19375  lsmmod  19605  rnghmresfn  20528  rnghmsscmap  20539  rhmresfn  20557  rhmsscmap  20568  rhmsubclem4  20597  acsfn1p  20708  lssacs  20873  lidlssbas  21123  zringlpirlem2  21373  zringlpirlem3  21374  asplss  21783  ressmplbas  21935  subrgmpl  21939  mplind  21977  ressply1bas  22113  pf1rcl  22236  ressply1evl  22257  evls1addd  22258  evls1muld  22259  evls1vsca  22260  evls1maprhm  22263  ofco2  22338  basdif0  22840  eltg4i  22847  ntrss2  22944  ntrin  22948  isopn3  22953  resttopon  23048  restuni2  23054  restcld  23059  restfpw  23066  neitr  23067  cnrest2r  23174  cnpresti  23175  cnprest  23176  lmss  23185  cnrmi  23247  restcnrm  23249  resthauslem  23250  imacmp  23284  fiuncmp  23291  subislly  23368  islly2  23371  cldllycmp  23382  hauspwdom  23388  kgeni  23424  llycmpkgen2  23437  ptbasfi  23468  ptclsg  23502  ptcnplem  23508  txtube  23527  txcmplem2  23529  txkgen  23539  kqdisj  23619  fbasrn  23771  trfg  23778  isufil2  23795  fmfnfmlem4  23844  hauspwpwf1  23874  txflf  23893  alexsubALTlem4  23937  tmdgsum2  23983  tsmsres  24031  tsmsxplem1  24040  ustexsym  24103  ustund  24109  trust  24117  utoptop  24122  restutop  24125  metrest  24412  restmetu  24458  tgioo  24684  reconnlem2  24716  cphsqrtcl  25084  tcphcph  25137  cfilresi  25195  caussi  25197  causs  25198  ovolfioo  25368  ovolficc  25369  ovolficcss  25370  ovolfsf  25372  ovollb  25380  ovolicc2lem1  25418  ovolicc2lem2  25419  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2  25423  nulmbl  25436  voliunlem1  25451  ovolfs2  25472  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombllem6  25489  uniioombl  25490  dyadmbllem  25500  dyadmbl  25501  opnmbllem  25502  volcn  25507  volivth  25508  mbfadd  25562  mbfsub  25563  i1fima  25579  i1fima2  25580  i1fd  25582  i1fadd  25596  i1fmul  25597  itg1addlem2  25598  itg1addlem4  25600  itg1addlem5  25601  i1fres  25606  mbfmul  25627  bddmulibl  25740  ellimc2  25778  ellimc3  25780  limcflf  25782  limcresi  25786  limciun  25795  dvreslem  25810  dvres2lem  25811  dvres3a  25815  cpnres  25839  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvmptres3  25860  lhop1lem  25918  rlimcnp2  26876  xrlimcnp  26878  chpchtsum  27130  2sqlem8  27337  2sqlem9  27338  rpvmasumlem  27398  rplogsum  27438  dirith2  27439  nosupbnd2  27628  axtgsegcon  28391  axtg5seg  28392  axtgbtwnid  28393  axtgpasch  28394  axtgcont1  28395  tglng  28473  chdmm1i  31406  chm0i  31419  ledii  31465  lejdii  31467  pjoml2i  31514  pjoml4i  31516  cmcmlem  31520  cmbr4i  31530  osumcori  31572  pjssmii  31610  mayete3i  31657  riesz4  31993  riesz1  31994  cnlnadjeu  32007  nmopadjlei  32017  pjclem1  32124  pjci  32129  mdbr3  32226  mdbr4  32227  dmdbr2  32232  dmdbr5  32237  ssmd2  32241  mdslj1i  32248  mdslj2i  32249  mdsl1i  32250  mdsl2bi  32252  mdslmd1lem1  32254  mdslmd1lem2  32255  mdslmd2i  32259  csmdsymi  32263  cvexchlem  32297  atomli  32311  atcvat4i  32326  difininv  32446  disjxpin  32517  imadifxp  32530  off2  32565  mptiffisupp  32616  indsumin  32785  indf1ofs  32789  resspos  32892  resstos  32893  submomnd  33024  suborng  33293  idlinsubrg  33402  ressply1invg  33538  evls1subd  33541  algextdeglem7  33713  algextdeglem8  33714  ordtrestNEW  33911  pnfneige0  33941  lmxrge0  33942  qqhnm  33980  qqhcn  33981  rrhre  34011  gsumesum  34049  esumlub  34050  esumcst  34053  esumpcvgval  34068  hasheuni  34075  esumcvg  34076  sigainb  34126  carsgclctunlem2  34310  sibfinima  34330  sibfof  34331  eulerpartlemelr  34348  eulerpartlemgh  34369  eulerpartlemgf  34370  eulerpartlemgs2  34371  eulerpartlemn  34372  probmeasb  34421  cndprob01  34426  hashreprin  34611  reprfi2  34614  breprexpnat  34625  hgt750lemd  34639  hgt750lema  34648  tgoldbachgtde  34651  tgoldbachgtda  34652  tgoldbachgt  34654  bnj1293  34806  connpconn  35222  iccllysconn  35237  cvmsss2  35261  cvmcov2  35262  cvmopnlem  35265  cvmliftmolem2  35269  cvmlift2lem12  35301  mvrsfpw  35493  elmsta  35535  msubvrs  35547  mclsind  35557  nepss  35705  dfon2lem4  35774  trer  36304  neiin  36320  neibastop1  36347  neibastop2lem  36348  topmeet  36352  filnetlem3  36368  weiunfr  36455  bj-disj2r  37016  bj-restpw  37080  bj-restb  37082  bj-restuni2  37086  bj-ablsscmn  37266  topdifinffinlem  37335  opnmbllem0  37650  mblfinlem4  37654  mbfposadd  37661  heibor1lem  37803  heiborlem1  37805  heiborlem3  37807  heiborlem10  37814  opidonOLD  37846  disjimin  38743  lshpinN  38982  lcvexchlem1  39027  lcvexchlem5  39031  pmod1i  39842  pmodN  39844  osumcllem7N  39956  pexmidlem4N  39967  dochdmj1  41384  dochexmidlem4  41457  lcfrlem25  41561  mapd1o  41642  mapdin  41656  elrfi  42682  elrfirn  42683  fnwe2lem2  43040  aomclem2  43044  lsmfgcl  43063  lmhmfgima  43073  lmhmfgsplit  43075  lmhmlnmsplit  43076  hbt  43119  ofoafg  43343  trrelind  43654  iunrelexp0  43691  isotone2  44038  grumnudlem  44274  ismnushort  44290  onfrALTlem3  44534  onfrALTlem2  44536  onfrALTlem3VD  44876  onfrALTlem2VD  44878  iunconnlem2  44924  wfac8prim  44992  restuni6  45116  disjinfi  45186  inmap  45203  fsumiunss  45573  islptre  45617  sumnnodd  45628  limcresiooub  45640  limcresioolb  45641  limcleqr  45642  limclner  45649  limclr  45653  limsuplesup  45697  limsuppnfdlem  45699  limsupres  45703  liminfgord  45752  liminfgf  45756  liminfcl  45761  limsupresxr  45764  liminfresxr  45765  liminfval2  45766  liminflelimsuplem  45773  liminfvalxr  45781  icccncfext  45885  fourierdlem20  46125  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem76  46180  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  fouriersw  46229  salgencntex  46341  sge0less  46390  sge0resplit  46404  sge0split  46407  sge0iunmptlemre  46413  sge0fodjrnlem  46414  caragencmpl  46533  ovolval2lem  46641  ovolval2  46642  ovolval3  46645  ovolval4lem2  46648  sssmf  46736  fcoreslem4  47067  fcoresf1  47070  fcoresfo  47072  3f1oss1  47076  rngchomrnghmresALTV  48267  termc  49508