Theorem inss2 4184

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

Syntax hints:   ∩ cin 3898   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-in 3906  df-ss 3916

This theorem is referenced by:  inindif  4322  difin0  4422  uniin  4883  iunxdif3  5046  relin2  5779  relres  5984  idssxp  6028  rnin  6120  ssrnres  6153  cnvrescnv  6171  ordin  6365  onfr  6374  ordelinel  6438  fnresin2  6636  fresaunres2  6725  ssimaex  6941  exfo  7075  ffvresb  7096  fnfvimad  7207  ofrfvalg  7657  ofval  7660  ofrval  7661  off  7667  ofres  7668  ofco  7674  fnwelem  8099  fnse  8101  fprlem1  8269  tfrlem5  8338  pmresg  8841  ixpfi2  9283  elfiun  9366  marypha1lem  9369  ordtypelem6  9461  ordtypelem7  9462  hartogslem1  9480  unxpwdom  9527  epfrs  9676  tcmin  9684  bnd2  9841  tskwe  9898  r0weon  9958  infxpenlem  9959  djuinf  10135  ackbij1lem9  10173  ackbij1lem10  10174  ackbij1lem15  10179  ackbij1lem16  10180  ackbij1b  10184  sdom2en01  10249  fin23lem26  10272  fin23lem13  10279  isfin1-3  10333  fin56  10340  fin1a2lem9  10355  brdom3  10475  brdom5  10476  brdom4  10477  fpwwe2lem11  10589  fpwwe2  10591  canthwelem  10598  gruima  10750  ingru  10763  gruina  10766  grur1a  10767  ltrelpi  10837  ltrelnq  10874  nqerf  10878  fzfi  13975  xptrrel  14983  rexanuz  15349  limsupgord  15475  limsupcl  15476  limsupgf  15478  limsupgle  15480  o1of2  15616  o1rlimmul  15622  ackbijnn  15834  bitsinv1  16452  bitsinvp1  16459  sadcaddlem  16467  sadadd2lem  16469  sadadd3  16471  sadaddlem  16476  sadasslem  16480  sadeq  16482  smupval  16498  prmrec  16934  structcnvcnv  17165  ressbasss  17251  ressbasssOLD  17252  ressress  17259  restsspw  17436  submre  17609  isacs1i  17665  rescabs  17842  resscat  17861  funcres2c  17912  ressffth  17949  catccatid  18115  catcisolem  18119  catciso  18120  yoniso  18293  resspos  18437  resstos  18438  acsinfd  18564  acsdomd  18565  tsrss  18597  idresefmnd  18909  idrespermg  19427  mvdco  19461  lsmmod  19691  submomnd  20148  rnghmresfn  20641  rnghmsscmap  20652  rhmresfn  20670  rhmsscmap  20681  rhmsubclem4  20710  acsfn1p  20821  suborng  20898  lssacs  21007  lidlssbas  21256  zringlpirlem2  21488  zringlpirlem3  21489  asplss  21898  ressmplbas  22053  subrgmpl  22057  mplind  22096  ressply1bas  22263  pf1rcl  22385  ressply1evl  22406  evls1addd  22407  evls1muld  22408  evls1vsca  22409  evls1maprhm  22412  ofco2  22484  basdif0  22986  eltg4i  22993  ntrss2  23090  ntrin  23094  isopn3  23099  resttopon  23194  restuni2  23200  restcld  23205  restfpw  23212  neitr  23213  cnrest2r  23320  cnpresti  23321  cnprest  23322  lmss  23331  cnrmi  23393  restcnrm  23395  resthauslem  23396  imacmp  23430  fiuncmp  23437  subislly  23514  islly2  23517  cldllycmp  23528  hauspwdom  23534  kgeni  23570  llycmpkgen2  23583  ptbasfi  23614  ptclsg  23648  ptcnplem  23654  txtube  23673  txcmplem2  23675  txkgen  23685  kqdisj  23765  fbasrn  23917  trfg  23924  isufil2  23941  fmfnfmlem4  23990  hauspwpwf1  24020  txflf  24039  alexsubALTlem4  24083  tmdgsum2  24129  tsmsres  24177  tsmsxplem1  24186  ustexsym  24249  ustund  24255  trust  24262  utoptop  24267  restutop  24270  metrest  24557  restmetu  24603  tgioo  24829  reconnlem2  24861  cphsqrtcl  25219  tcphcph  25272  cfilresi  25330  caussi  25332  causs  25333  ovolfioo  25502  ovolficc  25503  ovolficcss  25504  ovolfsf  25506  ovollb  25514  ovolicc2lem1  25552  ovolicc2lem2  25553  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2  25557  nulmbl  25570  voliunlem1  25585  ovolfs2  25606  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombllem6  25623  uniioombl  25624  dyadmbllem  25634  dyadmbl  25635  opnmbllem  25636  volcn  25641  volivth  25642  mbfadd  25696  mbfsub  25697  i1fima  25713  i1fima2  25714  i1fd  25716  i1fadd  25730  i1fmul  25731  itg1addlem2  25732  itg1addlem4  25734  itg1addlem5  25735  i1fres  25740  mbfmul  25761  bddmulibl  25874  ellimc2  25912  ellimc3  25914  limcflf  25916  limcresi  25920  limciun  25929  dvreslem  25944  dvres2lem  25945  dvres3a  25949  cpnres  25972  dvaddbr  25973  dvmulbr  25974  dvmptres3  25991  lhop1lem  26048  rlimcnp2  27001  xrlimcnp  27003  chpchtsum  27253  2sqlem8  27460  2sqlem9  27461  rpvmasumlem  27521  rplogsum  27561  dirith2  27562  nosupbnd2  27750  axtgsegcon  28603  axtg5seg  28604  axtgbtwnid  28605  axtgpasch  28606  axtgcont1  28607  tglng  28685  chdmm1i  31619  chm0i  31632  ledii  31678  lejdii  31680  pjoml2i  31727  pjoml4i  31729  cmcmlem  31733  cmbr4i  31743  osumcori  31785  pjssmii  31823  mayete3i  31870  riesz4  32206  riesz1  32207  cnlnadjeu  32220  nmopadjlei  32230  pjclem1  32337  pjci  32342  mdbr3  32439  mdbr4  32440  dmdbr2  32445  dmdbr5  32450  ssmd2  32454  mdslj1i  32461  mdslj2i  32462  mdsl1i  32463  mdsl2bi  32465  mdslmd1lem1  32467  mdslmd1lem2  32468  mdslmd2i  32472  csmdsymi  32476  cvexchlem  32510  atomli  32524  atcvat4i  32539  difininv  32658  disjxpin  32730  imadifxp  32743  off2  32786  mptiffisupp  32838  indsumin  32993  indf1ofs  32998  idlinsubrg  33571  ressply1invg  33719  evls1subd  33722  algextdeglem7  33974  algextdeglem8  33975  ordtrestNEW  34172  pnfneige0  34202  lmxrge0  34203  qqhnm  34241  qqhcn  34242  rrhre  34272  gsumesum  34310  esumlub  34311  esumcst  34314  esumpcvgval  34329  hasheuni  34336  esumcvg  34337  sigainb  34387  carsgclctunlem2  34570  sibfinima  34590  sibfof  34591  eulerpartlemelr  34608  eulerpartlemgh  34629  eulerpartlemgf  34630  eulerpartlemgs2  34631  eulerpartlemn  34632  probmeasb  34681  cndprob01  34686  hashreprin  34871  reprfi2  34874  breprexpnat  34885  hgt750lemd  34899  hgt750lema  34908  tgoldbachgtde  34911  tgoldbachgtda  34912  tgoldbachgt  34914  bnj1293  35068  connpconn  35533  iccllysconn  35548  cvmsss2  35572  cvmcov2  35573  cvmopnlem  35576  cvmliftmolem2  35580  cvmlift2lem12  35612  mvrsfpw  35804  elmsta  35846  msubvrs  35858  mclsind  35868  nepss  36016  dfon2lem4  36082  trer  36624  neiin  36640  neibastop1  36667  neibastop2lem  36668  topmeet  36672  filnetlem3  36688  weiunfr  36775  elttcirr  36839  bj-disj2r  37461  bj-restpw  37530  bj-restb  37532  bj-restuni2  37536  bj-ablsscmn  37718  topdifinffinlem  37789  opnmbllem0  38103  mblfinlem4  38107  mbfposadd  38114  heibor1lem  38256  heiborlem1  38258  heiborlem3  38260  heiborlem10  38267  opidonOLD  38299  disjimin  39298  lshpinN  39561  lcvexchlem1  39606  lcvexchlem5  39610  pmod1i  40420  pmodN  40422  osumcllem7N  40534  pexmidlem4N  40545  dochdmj1  41962  dochexmidlem4  42035  lcfrlem25  42139  mapd1o  42220  mapdin  42234  elrfi  43223  elrfirn  43224  fnwe2lem2  43576  aomclem2  43580  lsmfgcl  43599  lmhmfgima  43609  lmhmfgsplit  43611  lmhmlnmsplit  43612  hbt  43655  ofoafg  43879  trrelind  44189  iunrelexp0  44226  isotone2  44573  grumnudlem  44809  ismnushort  44825  onfrALTlem3  45068  onfrALTlem2  45070  onfrALTlem3VD  45410  onfrALTlem2VD  45412  iunconnlem2  45458  wfac8prim  45526  restuni6  45648  disjinfi  45718  inmap  45733  fsumiunss  46099  islptre  46143  sumnnodd  46154  limcresiooub  46164  limcresioolb  46165  limcleqr  46166  limclner  46173  limclr  46177  limsuplesup  46221  limsuppnfdlem  46223  limsupres  46227  liminfgord  46276  liminfgf  46280  liminfcl  46285  limsupresxr  46288  liminfresxr  46289  liminfval2  46290  liminflelimsuplem  46297  liminfvalxr  46305  icccncfext  46409  fourierdlem20  46649  fourierdlem48  46676  fourierdlem49  46677  fourierdlem50  46678  fourierdlem76  46704  fourierdlem103  46731  fourierdlem104  46732  fourierdlem113  46741  fouriersw  46753  salgencntex  46865  sge0less  46914  sge0resplit  46928  sge0split  46931  sge0iunmptlemre  46937  sge0fodjrnlem  46938  caragencmpl  47057  ovolval2lem  47165  ovolval2  47166  ovolval3  47169  ovolval4lem2  47172  sssmf  47260  nthrucw  47410  fcoreslem4  47608  fcoresf1  47611  fcoresfo  47613  3f1oss1  47617  rngchomrnghmresALTV  48849  termc  50088