Theorem inss2 4179

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 4150	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4178	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3970	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3889   ⊆ wss 3890

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 3391  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  inindif  4316  difin0  4415  iunxdif3  5038  relin2  5762  relres  5964  idssxp  6008  ssrnres  6136  cnvrescnv  6153  ordin  6347  onfr  6356  ordelinel  6420  fnresin2  6618  fresaunres2  6706  ssimaex  6919  exfo  7051  ffvresb  7072  fnfvimad  7182  ofrfvalg  7632  ofval  7635  ofrval  7636  off  7642  ofres  7643  ofco  7649  fnwelem  8074  fnse  8076  fprlem1  8243  tfrlem5  8312  pmresg  8811  ixpfi2  9253  elfiun  9336  marypha1lem  9339  ordtypelem6  9431  ordtypelem7  9432  hartogslem1  9450  unxpwdom  9497  epfrs  9643  tcmin  9651  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  10555  fpwwe2  10557  canthwelem  10564  gruima  10716  ingru  10729  gruina  10732  grur1a  10733  ltrelpi  10803  ltrelnq  10840  nqerf  10844  fzfi  13925  xptrrel  14933  rexanuz  15299  limsupgord  15425  limsupcl  15426  limsupgf  15428  limsupgle  15430  o1of2  15566  o1rlimmul  15572  ackbijnn  15784  bitsinv1  16402  bitsinvp1  16409  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  smupval  16448  prmrec  16884  structcnvcnv  17114  ressbasss  17200  ressbasssOLD  17201  ressress  17208  restsspw  17385  submre  17558  isacs1i  17614  rescabs  17791  resscat  17810  funcres2c  17861  ressffth  17898  catccatid  18064  catcisolem  18068  catciso  18069  yoniso  18242  resspos  18386  resstos  18387  acsinfd  18513  acsdomd  18514  tsrss  18546  idresefmnd  18858  idrespermg  19377  mvdco  19411  lsmmod  19641  submomnd  20098  rnghmresfn  20587  rnghmsscmap  20598  rhmresfn  20616  rhmsscmap  20627  rhmsubclem4  20656  acsfn1p  20767  suborng  20844  lssacs  20953  lidlssbas  21203  zringlpirlem2  21453  zringlpirlem3  21454  asplss  21863  ressmplbas  22016  subrgmpl  22020  mplind  22058  ressply1bas  22202  pf1rcl  22324  ressply1evl  22345  evls1addd  22346  evls1muld  22347  evls1vsca  22348  evls1maprhm  22351  ofco2  22426  basdif0  22928  eltg4i  22935  ntrss2  23032  ntrin  23036  isopn3  23041  resttopon  23136  restuni2  23142  restcld  23147  restfpw  23154  neitr  23155  cnrest2r  23262  cnpresti  23263  cnprest  23264  lmss  23273  cnrmi  23335  restcnrm  23337  resthauslem  23338  imacmp  23372  fiuncmp  23379  subislly  23456  islly2  23459  cldllycmp  23470  hauspwdom  23476  kgeni  23512  llycmpkgen2  23525  ptbasfi  23556  ptclsg  23590  ptcnplem  23596  txtube  23615  txcmplem2  23617  txkgen  23627  kqdisj  23707  fbasrn  23859  trfg  23866  isufil2  23883  fmfnfmlem4  23932  hauspwpwf1  23962  txflf  23981  alexsubALTlem4  24025  tmdgsum2  24071  tsmsres  24119  tsmsxplem1  24128  ustexsym  24191  ustund  24197  trust  24204  utoptop  24209  restutop  24212  metrest  24499  restmetu  24545  tgioo  24771  reconnlem2  24803  cphsqrtcl  25161  tcphcph  25214  cfilresi  25272  caussi  25274  causs  25275  ovolfioo  25444  ovolficc  25445  ovolficcss  25446  ovolfsf  25448  ovollb  25456  ovolicc2lem1  25494  ovolicc2lem2  25495  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2  25499  nulmbl  25512  voliunlem1  25527  ovolfs2  25548  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem2  25560  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombllem6  25565  uniioombl  25566  dyadmbllem  25576  dyadmbl  25577  opnmbllem  25578  volcn  25583  volivth  25584  mbfadd  25638  mbfsub  25639  i1fima  25655  i1fima2  25656  i1fd  25658  i1fadd  25672  i1fmul  25673  itg1addlem2  25674  itg1addlem4  25676  itg1addlem5  25677  i1fres  25682  mbfmul  25703  bddmulibl  25816  ellimc2  25854  ellimc3  25856  limcflf  25858  limcresi  25862  limciun  25871  dvreslem  25886  dvres2lem  25887  dvres3a  25891  cpnres  25914  dvaddbr  25915  dvmulbr  25916  dvmptres3  25933  lhop1lem  25990  rlimcnp2  26943  xrlimcnp  26945  chpchtsum  27196  2sqlem8  27403  2sqlem9  27404  rpvmasumlem  27464  rplogsum  27504  dirith2  27505  nosupbnd2  27694  axtgsegcon  28546  axtg5seg  28547  axtgbtwnid  28548  axtgpasch  28549  axtgcont1  28550  tglng  28628  chdmm1i  31563  chm0i  31576  ledii  31622  lejdii  31624  pjoml2i  31671  pjoml4i  31673  cmcmlem  31677  cmbr4i  31687  osumcori  31729  pjssmii  31767  mayete3i  31814  riesz4  32150  riesz1  32151  cnlnadjeu  32164  nmopadjlei  32174  pjclem1  32281  pjci  32286  mdbr3  32383  mdbr4  32384  dmdbr2  32389  dmdbr5  32394  ssmd2  32398  mdslj1i  32405  mdslj2i  32406  mdsl1i  32407  mdsl2bi  32409  mdslmd1lem1  32411  mdslmd1lem2  32412  mdslmd2i  32416  csmdsymi  32420  cvexchlem  32454  atomli  32468  atcvat4i  32483  difininv  32602  disjxpin  32673  imadifxp  32686  off2  32729  mptiffisupp  32781  indsumin  32936  indf1ofs  32941  idlinsubrg  33506  ressply1invg  33644  evls1subd  33647  algextdeglem7  33883  algextdeglem8  33884  ordtrestNEW  34081  pnfneige0  34111  lmxrge0  34112  qqhnm  34150  qqhcn  34151  rrhre  34181  gsumesum  34219  esumlub  34220  esumcst  34223  esumpcvgval  34238  hasheuni  34245  esumcvg  34246  sigainb  34296  carsgclctunlem2  34479  sibfinima  34499  sibfof  34500  eulerpartlemelr  34517  eulerpartlemgh  34538  eulerpartlemgf  34539  eulerpartlemgs2  34540  eulerpartlemn  34541  probmeasb  34590  cndprob01  34595  hashreprin  34780  reprfi2  34783  breprexpnat  34794  hgt750lemd  34808  hgt750lema  34817  tgoldbachgtde  34820  tgoldbachgtda  34821  tgoldbachgt  34823  bnj1293  34974  connpconn  35433  iccllysconn  35448  cvmsss2  35472  cvmcov2  35473  cvmopnlem  35476  cvmliftmolem2  35480  cvmlift2lem12  35512  mvrsfpw  35704  elmsta  35746  msubvrs  35758  mclsind  35768  nepss  35916  dfon2lem4  35982  trer  36514  neiin  36530  neibastop1  36557  neibastop2lem  36558  topmeet  36562  filnetlem3  36578  weiunfr  36665  elttcirr  36729  bj-disj2r  37351  bj-restpw  37420  bj-restb  37422  bj-restuni2  37426  bj-ablsscmn  37608  topdifinffinlem  37677  opnmbllem0  37991  mblfinlem4  37995  mbfposadd  38002  heibor1lem  38144  heiborlem1  38146  heiborlem3  38148  heiborlem10  38155  opidonOLD  38187  disjimin  39186  lshpinN  39449  lcvexchlem1  39494  lcvexchlem5  39498  pmod1i  40308  pmodN  40310  osumcllem7N  40422  pexmidlem4N  40433  dochdmj1  41850  dochexmidlem4  41923  lcfrlem25  42027  mapd1o  42108  mapdin  42122  elrfi  43140  elrfirn  43141  fnwe2lem2  43497  aomclem2  43501  lsmfgcl  43520  lmhmfgima  43530  lmhmfgsplit  43532  lmhmlnmsplit  43533  hbt  43576  ofoafg  43800  trrelind  44110  iunrelexp0  44147  isotone2  44494  grumnudlem  44730  ismnushort  44746  onfrALTlem3  44989  onfrALTlem2  44991  onfrALTlem3VD  45331  onfrALTlem2VD  45333  iunconnlem2  45379  wfac8prim  45447  restuni6  45570  disjinfi  45640  inmap  45656  fsumiunss  46023  islptre  46067  sumnnodd  46078  limcresiooub  46088  limcresioolb  46089  limcleqr  46090  limclner  46097  limclr  46101  limsuplesup  46145  limsuppnfdlem  46147  limsupres  46151  liminfgord  46200  liminfgf  46204  liminfcl  46209  limsupresxr  46212  liminfresxr  46213  liminfval2  46214  liminflelimsuplem  46221  liminfvalxr  46229  icccncfext  46333  fourierdlem20  46573  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem76  46628  fourierdlem103  46655  fourierdlem104  46656  fourierdlem113  46665  fouriersw  46677  salgencntex  46789  sge0less  46838  sge0resplit  46852  sge0split  46855  sge0iunmptlemre  46861  sge0fodjrnlem  46862  caragencmpl  46981  ovolval2lem  47089  ovolval2  47090  ovolval3  47093  ovolval4lem2  47096  sssmf  47184  nthrucw  47332  fcoreslem4  47526  fcoresf1  47529  fcoresfo  47531  3f1oss1  47535  rngchomrnghmresALTV  48767  termc  50006