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

Syntax hints:   ∩ cin 3897   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-in 3905  df-ss 3915

This theorem is referenced by:  inindif  4324  difin0  4423  iunxdif3  5047  relin2  5759  relres  5961  idssxp  6005  ssrnres  6133  cnvrescnv  6150  ordin  6344  onfr  6353  ordelinel  6417  fnresin2  6615  fresaunres2  6703  ssimaex  6916  exfo  7047  ffvresb  7067  fnfvimad  7177  ofrfvalg  7627  ofval  7630  ofrval  7631  off  7637  ofres  7638  ofco  7644  fnwelem  8070  fnse  8072  fprlem1  8239  tfrlem5  8308  pmresg  8804  ixpfi2  9245  elfiun  9325  marypha1lem  9328  ordtypelem6  9420  ordtypelem7  9421  hartogslem1  9439  unxpwdom  9486  epfrs  9632  tcmin  9640  bnd2  9797  tskwe  9854  r0weon  9914  infxpenlem  9915  djuinf  10091  ackbij1lem9  10129  ackbij1lem10  10130  ackbij1lem15  10135  ackbij1lem16  10136  ackbij1b  10140  sdom2en01  10204  fin23lem26  10227  fin23lem13  10234  isfin1-3  10288  fin56  10295  fin1a2lem9  10310  brdom3  10430  brdom5  10431  brdom4  10432  fpwwe2lem11  10543  fpwwe2  10545  canthwelem  10552  gruima  10704  ingru  10717  gruina  10720  grur1a  10721  ltrelpi  10791  ltrelnq  10828  nqerf  10832  fzfi  13886  xptrrel  14894  rexanuz  15260  limsupgord  15386  limsupcl  15387  limsupgf  15389  limsupgle  15391  o1of2  15527  o1rlimmul  15533  ackbijnn  15742  bitsinv1  16360  bitsinvp1  16367  sadcaddlem  16375  sadadd2lem  16377  sadadd3  16379  sadaddlem  16384  sadasslem  16388  sadeq  16390  smupval  16406  prmrec  16841  structcnvcnv  17071  ressbasss  17157  ressbasssOLD  17158  ressress  17165  restsspw  17342  submre  17515  isacs1i  17571  rescabs  17748  resscat  17767  funcres2c  17818  ressffth  17855  catccatid  18021  catcisolem  18025  catciso  18026  yoniso  18199  resspos  18343  resstos  18344  acsinfd  18470  acsdomd  18471  tsrss  18503  idresefmnd  18815  idrespermg  19331  mvdco  19365  lsmmod  19595  submomnd  20052  rnghmresfn  20543  rnghmsscmap  20554  rhmresfn  20572  rhmsscmap  20583  rhmsubclem4  20612  acsfn1p  20723  suborng  20800  lssacs  20909  lidlssbas  21159  zringlpirlem2  21409  zringlpirlem3  21410  asplss  21820  ressmplbas  21974  subrgmpl  21978  mplind  22016  ressply1bas  22160  pf1rcl  22284  ressply1evl  22305  evls1addd  22306  evls1muld  22307  evls1vsca  22308  evls1maprhm  22311  ofco2  22386  basdif0  22888  eltg4i  22895  ntrss2  22992  ntrin  22996  isopn3  23001  resttopon  23096  restuni2  23102  restcld  23107  restfpw  23114  neitr  23115  cnrest2r  23222  cnpresti  23223  cnprest  23224  lmss  23233  cnrmi  23295  restcnrm  23297  resthauslem  23298  imacmp  23332  fiuncmp  23339  subislly  23416  islly2  23419  cldllycmp  23430  hauspwdom  23436  kgeni  23472  llycmpkgen2  23485  ptbasfi  23516  ptclsg  23550  ptcnplem  23556  txtube  23575  txcmplem2  23577  txkgen  23587  kqdisj  23667  fbasrn  23819  trfg  23826  isufil2  23843  fmfnfmlem4  23892  hauspwpwf1  23922  txflf  23941  alexsubALTlem4  23985  tmdgsum2  24031  tsmsres  24079  tsmsxplem1  24088  ustexsym  24151  ustund  24157  trust  24164  utoptop  24169  restutop  24172  metrest  24459  restmetu  24505  tgioo  24731  reconnlem2  24763  cphsqrtcl  25131  tcphcph  25184  cfilresi  25242  caussi  25244  causs  25245  ovolfioo  25415  ovolficc  25416  ovolficcss  25417  ovolfsf  25419  ovollb  25427  ovolicc2lem1  25465  ovolicc2lem2  25466  ovolicc2lem3  25467  ovolicc2lem4  25468  ovolicc2  25470  nulmbl  25483  voliunlem1  25498  ovolfs2  25519  uniiccdif  25526  uniioovol  25527  uniiccvol  25528  uniioombllem2  25531  uniioombllem3a  25532  uniioombllem3  25533  uniioombllem4  25534  uniioombllem5  25535  uniioombllem6  25536  uniioombl  25537  dyadmbllem  25547  dyadmbl  25548  opnmbllem  25549  volcn  25554  volivth  25555  mbfadd  25609  mbfsub  25610  i1fima  25626  i1fima2  25627  i1fd  25629  i1fadd  25643  i1fmul  25644  itg1addlem2  25645  itg1addlem4  25647  itg1addlem5  25648  i1fres  25653  mbfmul  25674  bddmulibl  25787  ellimc2  25825  ellimc3  25827  limcflf  25829  limcresi  25833  limciun  25842  dvreslem  25857  dvres2lem  25858  dvres3a  25862  cpnres  25886  dvaddbr  25887  dvmulbr  25888  dvmulbrOLD  25889  dvmptres3  25907  lhop1lem  25965  rlimcnp2  26923  xrlimcnp  26925  chpchtsum  27177  2sqlem8  27384  2sqlem9  27385  rpvmasumlem  27445  rplogsum  27485  dirith2  27486  nosupbnd2  27675  axtgsegcon  28462  axtg5seg  28463  axtgbtwnid  28464  axtgpasch  28465  axtgcont1  28466  tglng  28544  chdmm1i  31478  chm0i  31491  ledii  31537  lejdii  31539  pjoml2i  31586  pjoml4i  31588  cmcmlem  31592  cmbr4i  31602  osumcori  31644  pjssmii  31682  mayete3i  31729  riesz4  32065  riesz1  32066  cnlnadjeu  32079  nmopadjlei  32089  pjclem1  32196  pjci  32201  mdbr3  32298  mdbr4  32299  dmdbr2  32304  dmdbr5  32309  ssmd2  32313  mdslj1i  32320  mdslj2i  32321  mdsl1i  32322  mdsl2bi  32324  mdslmd1lem1  32326  mdslmd1lem2  32327  mdslmd2i  32331  csmdsymi  32335  cvexchlem  32369  atomli  32383  atcvat4i  32398  difininv  32518  disjxpin  32589  imadifxp  32602  off2  32645  mptiffisupp  32698  indsumin  32871  indf1ofs  32876  idlinsubrg  33440  ressply1invg  33578  evls1subd  33581  algextdeglem7  33808  algextdeglem8  33809  ordtrestNEW  34006  pnfneige0  34036  lmxrge0  34037  qqhnm  34075  qqhcn  34076  rrhre  34106  gsumesum  34144  esumlub  34145  esumcst  34148  esumpcvgval  34163  hasheuni  34170  esumcvg  34171  sigainb  34221  carsgclctunlem2  34404  sibfinima  34424  sibfof  34425  eulerpartlemelr  34442  eulerpartlemgh  34463  eulerpartlemgf  34464  eulerpartlemgs2  34465  eulerpartlemn  34466  probmeasb  34515  cndprob01  34520  hashreprin  34705  reprfi2  34708  breprexpnat  34719  hgt750lemd  34733  hgt750lema  34742  tgoldbachgtde  34745  tgoldbachgtda  34746  tgoldbachgt  34748  bnj1293  34900  connpconn  35351  iccllysconn  35366  cvmsss2  35390  cvmcov2  35391  cvmopnlem  35394  cvmliftmolem2  35398  cvmlift2lem12  35430  mvrsfpw  35622  elmsta  35664  msubvrs  35676  mclsind  35686  nepss  35834  dfon2lem4  35900  trer  36432  neiin  36448  neibastop1  36475  neibastop2lem  36476  topmeet  36480  filnetlem3  36496  weiunfr  36583  bj-disj2r  37145  bj-restpw  37209  bj-restb  37211  bj-restuni2  37215  bj-ablsscmn  37395  topdifinffinlem  37464  opnmbllem0  37769  mblfinlem4  37773  mbfposadd  37780  heibor1lem  37922  heiborlem1  37924  heiborlem3  37926  heiborlem10  37933  opidonOLD  37965  disjimin  38922  lshpinN  39161  lcvexchlem1  39206  lcvexchlem5  39210  pmod1i  40020  pmodN  40022  osumcllem7N  40134  pexmidlem4N  40145  dochdmj1  41562  dochexmidlem4  41635  lcfrlem25  41739  mapd1o  41820  mapdin  41834  elrfi  42851  elrfirn  42852  fnwe2lem2  43208  aomclem2  43212  lsmfgcl  43231  lmhmfgima  43241  lmhmfgsplit  43243  lmhmlnmsplit  43244  hbt  43287  ofoafg  43511  trrelind  43822  iunrelexp0  43859  isotone2  44206  grumnudlem  44442  ismnushort  44458  onfrALTlem3  44701  onfrALTlem2  44703  onfrALTlem3VD  45043  onfrALTlem2VD  45045  iunconnlem2  45091  wfac8prim  45159  restuni6  45282  disjinfi  45352  inmap  45369  fsumiunss  45737  islptre  45781  sumnnodd  45792  limcresiooub  45802  limcresioolb  45803  limcleqr  45804  limclner  45811  limclr  45815  limsuplesup  45859  limsuppnfdlem  45861  limsupres  45865  liminfgord  45914  liminfgf  45918  liminfcl  45923  limsupresxr  45926  liminfresxr  45927  liminfval2  45928  liminflelimsuplem  45935  liminfvalxr  45943  icccncfext  46047  fourierdlem20  46287  fourierdlem48  46314  fourierdlem49  46315  fourierdlem50  46316  fourierdlem76  46342  fourierdlem103  46369  fourierdlem104  46370  fourierdlem113  46379  fouriersw  46391  salgencntex  46503  sge0less  46552  sge0resplit  46566  sge0split  46569  sge0iunmptlemre  46575  sge0fodjrnlem  46576  caragencmpl  46695  ovolval2lem  46803  ovolval2  46804  ovolval3  46807  ovolval4lem2  46810  sssmf  46898  nthrucw  47046  fcoreslem4  47228  fcoresf1  47231  fcoresfo  47233  3f1oss1  47237  rngchomrnghmresALTV  48441  termc  49680