Theorem inss2 4190

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 4161	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4189	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3981	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3900   ⊆ wss 3901

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  inindif  4327  difin0  4426  iunxdif3  5050  relin2  5762  relres  5964  idssxp  6008  ssrnres  6136  cnvrescnv  6153  ordin  6347  onfr  6356  ordelinel  6420  fnresin2  6618  fresaunres2  6706  ssimaex  6919  exfo  7050  ffvresb  7070  fnfvimad  7180  ofrfvalg  7630  ofval  7633  ofrval  7634  off  7640  ofres  7641  ofco  7647  fnwelem  8073  fnse  8075  fprlem1  8242  tfrlem5  8311  pmresg  8808  ixpfi2  9250  elfiun  9333  marypha1lem  9336  ordtypelem6  9428  ordtypelem7  9429  hartogslem1  9447  unxpwdom  9494  epfrs  9640  tcmin  9648  bnd2  9805  tskwe  9862  r0weon  9922  infxpenlem  9923  djuinf  10099  ackbij1lem9  10137  ackbij1lem10  10138  ackbij1lem15  10143  ackbij1lem16  10144  ackbij1b  10148  sdom2en01  10212  fin23lem26  10235  fin23lem13  10242  isfin1-3  10296  fin56  10303  fin1a2lem9  10318  brdom3  10438  brdom5  10439  brdom4  10440  fpwwe2lem11  10552  fpwwe2  10554  canthwelem  10561  gruima  10713  ingru  10726  gruina  10729  grur1a  10730  ltrelpi  10800  ltrelnq  10837  nqerf  10841  fzfi  13895  xptrrel  14903  rexanuz  15269  limsupgord  15395  limsupcl  15396  limsupgf  15398  limsupgle  15400  o1of2  15536  o1rlimmul  15542  ackbijnn  15751  bitsinv1  16369  bitsinvp1  16376  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  sadeq  16399  smupval  16415  prmrec  16850  structcnvcnv  17080  ressbasss  17166  ressbasssOLD  17167  ressress  17174  restsspw  17351  submre  17524  isacs1i  17580  rescabs  17757  resscat  17776  funcres2c  17827  ressffth  17864  catccatid  18030  catcisolem  18034  catciso  18035  yoniso  18208  resspos  18352  resstos  18353  acsinfd  18479  acsdomd  18480  tsrss  18512  idresefmnd  18824  idrespermg  19340  mvdco  19374  lsmmod  19604  submomnd  20061  rnghmresfn  20552  rnghmsscmap  20563  rhmresfn  20581  rhmsscmap  20592  rhmsubclem4  20621  acsfn1p  20732  suborng  20809  lssacs  20918  lidlssbas  21168  zringlpirlem2  21418  zringlpirlem3  21419  asplss  21829  ressmplbas  21983  subrgmpl  21987  mplind  22025  ressply1bas  22169  pf1rcl  22293  ressply1evl  22314  evls1addd  22315  evls1muld  22316  evls1vsca  22317  evls1maprhm  22320  ofco2  22395  basdif0  22897  eltg4i  22904  ntrss2  23001  ntrin  23005  isopn3  23010  resttopon  23105  restuni2  23111  restcld  23116  restfpw  23123  neitr  23124  cnrest2r  23231  cnpresti  23232  cnprest  23233  lmss  23242  cnrmi  23304  restcnrm  23306  resthauslem  23307  imacmp  23341  fiuncmp  23348  subislly  23425  islly2  23428  cldllycmp  23439  hauspwdom  23445  kgeni  23481  llycmpkgen2  23494  ptbasfi  23525  ptclsg  23559  ptcnplem  23565  txtube  23584  txcmplem2  23586  txkgen  23596  kqdisj  23676  fbasrn  23828  trfg  23835  isufil2  23852  fmfnfmlem4  23901  hauspwpwf1  23931  txflf  23950  alexsubALTlem4  23994  tmdgsum2  24040  tsmsres  24088  tsmsxplem1  24097  ustexsym  24160  ustund  24166  trust  24173  utoptop  24178  restutop  24181  metrest  24468  restmetu  24514  tgioo  24740  reconnlem2  24772  cphsqrtcl  25140  tcphcph  25193  cfilresi  25251  caussi  25253  causs  25254  ovolfioo  25424  ovolficc  25425  ovolficcss  25426  ovolfsf  25428  ovollb  25436  ovolicc2lem1  25474  ovolicc2lem2  25475  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2  25479  nulmbl  25492  voliunlem1  25507  ovolfs2  25528  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombllem6  25545  uniioombl  25546  dyadmbllem  25556  dyadmbl  25557  opnmbllem  25558  volcn  25563  volivth  25564  mbfadd  25618  mbfsub  25619  i1fima  25635  i1fima2  25636  i1fd  25638  i1fadd  25652  i1fmul  25653  itg1addlem2  25654  itg1addlem4  25656  itg1addlem5  25657  i1fres  25662  mbfmul  25683  bddmulibl  25796  ellimc2  25834  ellimc3  25836  limcflf  25838  limcresi  25842  limciun  25851  dvreslem  25866  dvres2lem  25867  dvres3a  25871  cpnres  25895  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvmptres3  25916  lhop1lem  25974  rlimcnp2  26932  xrlimcnp  26934  chpchtsum  27186  2sqlem8  27393  2sqlem9  27394  rpvmasumlem  27454  rplogsum  27494  dirith2  27495  nosupbnd2  27684  axtgsegcon  28536  axtg5seg  28537  axtgbtwnid  28538  axtgpasch  28539  axtgcont1  28540  tglng  28618  chdmm1i  31552  chm0i  31565  ledii  31611  lejdii  31613  pjoml2i  31660  pjoml4i  31662  cmcmlem  31666  cmbr4i  31676  osumcori  31718  pjssmii  31756  mayete3i  31803  riesz4  32139  riesz1  32140  cnlnadjeu  32153  nmopadjlei  32163  pjclem1  32270  pjci  32275  mdbr3  32372  mdbr4  32373  dmdbr2  32378  dmdbr5  32383  ssmd2  32387  mdslj1i  32394  mdslj2i  32395  mdsl1i  32396  mdsl2bi  32398  mdslmd1lem1  32400  mdslmd1lem2  32401  mdslmd2i  32405  csmdsymi  32409  cvexchlem  32443  atomli  32457  atcvat4i  32472  difininv  32592  disjxpin  32663  imadifxp  32676  off2  32719  mptiffisupp  32772  indsumin  32943  indf1ofs  32948  idlinsubrg  33512  ressply1invg  33650  evls1subd  33653  algextdeglem7  33880  algextdeglem8  33881  ordtrestNEW  34078  pnfneige0  34108  lmxrge0  34109  qqhnm  34147  qqhcn  34148  rrhre  34178  gsumesum  34216  esumlub  34217  esumcst  34220  esumpcvgval  34235  hasheuni  34242  esumcvg  34243  sigainb  34293  carsgclctunlem2  34476  sibfinima  34496  sibfof  34497  eulerpartlemelr  34514  eulerpartlemgh  34535  eulerpartlemgf  34536  eulerpartlemgs2  34537  eulerpartlemn  34538  probmeasb  34587  cndprob01  34592  hashreprin  34777  reprfi2  34780  breprexpnat  34791  hgt750lemd  34805  hgt750lema  34814  tgoldbachgtde  34817  tgoldbachgtda  34818  tgoldbachgt  34820  bnj1293  34972  connpconn  35429  iccllysconn  35444  cvmsss2  35468  cvmcov2  35469  cvmopnlem  35472  cvmliftmolem2  35476  cvmlift2lem12  35508  mvrsfpw  35700  elmsta  35742  msubvrs  35754  mclsind  35764  nepss  35912  dfon2lem4  35978  trer  36510  neiin  36526  neibastop1  36553  neibastop2lem  36554  topmeet  36558  filnetlem3  36574  weiunfr  36661  bj-disj2r  37229  bj-restpw  37297  bj-restb  37299  bj-restuni2  37303  bj-ablsscmn  37483  topdifinffinlem  37552  opnmbllem0  37857  mblfinlem4  37861  mbfposadd  37868  heibor1lem  38010  heiborlem1  38012  heiborlem3  38014  heiborlem10  38021  opidonOLD  38053  disjimin  39010  lshpinN  39249  lcvexchlem1  39294  lcvexchlem5  39298  pmod1i  40108  pmodN  40110  osumcllem7N  40222  pexmidlem4N  40233  dochdmj1  41650  dochexmidlem4  41723  lcfrlem25  41827  mapd1o  41908  mapdin  41922  elrfi  42936  elrfirn  42937  fnwe2lem2  43293  aomclem2  43297  lsmfgcl  43316  lmhmfgima  43326  lmhmfgsplit  43328  lmhmlnmsplit  43329  hbt  43372  ofoafg  43596  trrelind  43906  iunrelexp0  43943  isotone2  44290  grumnudlem  44526  ismnushort  44542  onfrALTlem3  44785  onfrALTlem2  44787  onfrALTlem3VD  45127  onfrALTlem2VD  45129  iunconnlem2  45175  wfac8prim  45243  restuni6  45366  disjinfi  45436  inmap  45453  fsumiunss  45821  islptre  45865  sumnnodd  45876  limcresiooub  45886  limcresioolb  45887  limcleqr  45888  limclner  45895  limclr  45899  limsuplesup  45943  limsuppnfdlem  45945  limsupres  45949  liminfgord  45998  liminfgf  46002  liminfcl  46007  limsupresxr  46010  liminfresxr  46011  liminfval2  46012  liminflelimsuplem  46019  liminfvalxr  46027  icccncfext  46131  fourierdlem20  46371  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem76  46426  fourierdlem103  46453  fourierdlem104  46454  fourierdlem113  46463  fouriersw  46475  salgencntex  46587  sge0less  46636  sge0resplit  46650  sge0split  46653  sge0iunmptlemre  46659  sge0fodjrnlem  46660  caragencmpl  46779  ovolval2lem  46887  ovolval2  46888  ovolval3  46891  ovolval4lem2  46894  sssmf  46982  nthrucw  47130  fcoreslem4  47312  fcoresf1  47315  fcoresfo  47317  3f1oss1  47321  rngchomrnghmresALTV  48525  termc  49764