Theorem inss2 4183

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

This proof depends on syntax axioms:   ∩ cin 3898   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916

This theorem is used by:  inindif  4324  vvin  4359  difin0  4428  uniin  4891  iunxdif3  5055  relin2  5794  relres  5998  idssxp  6045  rnin  6137  ssrnres  6171  cnvrescnv  6189  ordin  6388  onfr  6397  ordelinel  6461  fnresin2  6658  fresaunres2  6747  ssimaex  6963  exfo  7098  ffvresb  7119  fnfvimad  7233  ofrfvalg  7686  ofval  7689  ofrval  7690  off  7696  ofres  7697  ofco  7703  fnwelem  8129  fnse  8131  fprlem1  8299  tfrlem5  8368  pmresg  8877  ixpfi2  9317  elfiun  9400  marypha1lem  9403  ordtypelem6  9495  ordtypelem7  9496  hartogslem1  9514  unxpwdom  9561  epfrs  9710  tcmin  9718  bnd2  9895  tskwe  9955  r0weon  10015  infxpenlem  10016  djuinf  10191  ackbij1lem9  10229  ackbij1lem10  10230  ackbij1lem15  10235  ackbij1lem16  10236  ackbij1b  10240  sdom2en01  10304  fin23lem26  10327  fin23lem13  10334  isfin1-3  10388  fin56  10395  fin1a2lem9  10410  brdom3  10531  brdom5  10532  brdom4  10533  fpwwe2lem11  10650  fpwwe2  10652  canthwelem  10659  gruima  10811  ingru  10824  gruina  10827  grur1a  10828  ltrelpi  10898  ltrelnq  10935  nqerf  10939  fzfi  14036  xptrrel  15053  rexanuz  15433  limsupgord  15559  limsupcl  15560  limsupgf  15562  limsupgle  15564  o1of2  15700  o1rlimmul  15706  ackbijnn  15917  bitsinv1  16532  bitsinvp1  16539  sadcaddlem  16547  sadadd2lem  16549  sadadd3  16551  sadaddlem  16556  sadasslem  16560  sadeq  16562  smupval  16578  prmrec  17014  structcnvcnv  17245  ressbasss  17331  ressbasssOLD  17332  ressress  17339  restsspw  17516  submre  17689  isacs1i  17745  rescabs  17922  resscat  17941  funcres2c  17992  ressffth  18029  catccatid  18195  catcisolem  18199  catciso  18200  yoniso  18373  resspos  18517  resstos  18518  acsinfd  18644  acsdomd  18645  tsrss  18677  idresefmnd  19008  idrespermg  19538  mvdco  19572  lsmmod  19802  submomnd  20259  rnghmresfn  20781  rnghmsscmap  20792  rhmresfn  20810  rhmsscmap  20821  rhmsubclem4  20850  acsfn1p  20965  suborng  21042  lssacs  21151  lidlssbas  21401  zringlpirlem2  21676  zringlpirlem3  21677  asplss  22088  ressmplbas  22243  subrgmpl  22247  mplind  22286  ressply1bas  22453  pf1rcl  22574  ressply1evl  22595  evls1addd  22596  evls1muld  22597  evls1vsca  22598  evls1maprhm  22601  ofco2  22673  basdif0  23178  eltg4i  23185  ntrss2  23282  ntrin  23286  isopn3  23291  resttopon  23386  restuni2  23392  restcld  23397  restfpw  23404  neitr  23405  cnrest2r  23512  cnpresti  23513  cnprest  23514  lmss  23523  cnrmi  23585  restcnrm  23587  resthauslem  23588  imacmp  23622  fiuncmp  23629  subislly  23707  islly2  23710  cldllycmp  23721  hauspwdom  23727  kgeni  23763  llycmpkgen2  23776  ptbasfi  23807  ptclsg  23841  ptcnplem  23847  txtube  23866  txcmplem2  23868  txkgen  23878  kqdisj  23958  fbasrn  24110  trfg  24117  isufil2  24134  fmfnfmlem4  24183  hauspwpwf1  24213  txflf  24232  alexsubALTlem4  24276  tmdgsum2  24322  tsmsres  24370  tsmsxplem1  24379  ustexsym  24442  ustund  24448  trust  24455  utoptop  24460  restutop  24463  metrest  24750  restmetu  24796  tgioo  25022  reconnlem2  25054  cphsqrtcl  25412  tcphcph  25465  cfilresi  25523  caussi  25525  causs  25526  ovolfioo  25695  ovolficc  25696  ovolficcss  25697  ovolfsf  25699  ovollb  25707  ovolicc2lem1  25745  ovolicc2lem2  25746  ovolicc2lem3  25747  ovolicc2lem4  25748  ovolicc2  25750  nulmbl  25763  voliunlem1  25778  ovolfs2  25799  uniiccdif  25806  uniioovol  25807  uniiccvol  25808  uniioombllem2  25811  uniioombllem3a  25812  uniioombllem3  25813  uniioombllem4  25814  uniioombllem5  25815  uniioombllem6  25816  uniioombl  25817  dyadmbllem  25827  dyadmbl  25828  opnmbllem  25829  volcn  25834  volivth  25835  mbfadd  25889  mbfsub  25890  i1fima  25906  i1fima2  25907  i1fd  25909  i1fadd  25923  i1fmul  25924  itg1addlem2  25925  itg1addlem4  25927  itg1addlem5  25928  i1fres  25933  mbfmul  25954  bddmulibl  26066  ellimc2  26104  ellimc3  26106  limcflf  26108  limcresi  26112  limciun  26121  dvreslem  26136  dvres2lem  26137  dvres3a  26141  cpnres  26164  dvaddbr  26165  dvmulbr  26166  dvmptres3  26183  lhop1lem  26240  rlimcnp2  27203  xrlimcnp  27205  chpchtsum  27455  2sqlem8  27662  2sqlem9  27663  rpvmasumlem  27723  rplogsum  27763  dirith2  27764  nosupbnd2  27952  axtgsegcon  28805  axtg5seg  28806  axtgbtwnid  28807  axtgpasch  28808  axtgcont1  28809  tglng  28888  chdmm1i  31958  chm0i  31971  ledii  32017  lejdii  32019  pjoml2i  32066  pjoml4i  32068  cmcmlem  32072  cmbr4i  32082  osumcori  32124  pjssmii  32162  mayete3i  32209  riesz4  32545  riesz1  32546  cnlnadjeu  32559  nmopadjlei  32569  pjclem1  32676  pjci  32681  mdbr3  32778  mdbr4  32779  dmdbr2  32784  dmdbr5  32789  ssmd2  32793  mdslj1i  32800  mdslj2i  32801  mdsl1i  32802  mdsl2bi  32804  mdslmd1lem1  32806  mdslmd1lem2  32807  mdslmd2i  32811  csmdsymi  32815  cvexchlem  32849  atomli  32863  atcvat4i  32878  difininv  32992  disjxpin  33061  imadifxp  33074  off2  33114  mptiffisupp  33165  indsumin  33307  indf1ofs  33312  idlinsubrg  33859  ressply1invg  33979  evls1subd  33982  algextdeglem7  34233  algextdeglem8  34234  ordtrestNEW  34431  pnfneige0  34461  lmxrge0  34462  qqhnm  34500  qqhcn  34501  rrhre  34531  gsumesum  34569  esumlub  34570  esumcst  34573  esumpcvgval  34588  hasheuni  34595  esumcvg  34596  sigainb  34647  carsgclctunlem2  34830  sibfinima  34850  sibfof  34851  eulerpartlemelr  34868  eulerpartlemgh  34889  eulerpartlemgf  34890  eulerpartlemgs2  34891  eulerpartlemn  34892  probmeasb  34941  cndprob01  34946  hashreprin  35128  reprfi2  35131  breprexpnat  35142  hgt750lemd  35156  hgt750lema  35165  tgoldbachgtde  35168  tgoldbachgtda  35169  tgoldbachgt  35171  bnj1293  35325  connpconn  35814  iccllysconn  35829  cvmsss2  35853  cvmcov2  35854  cvmopnlem  35857  cvmliftmolem2  35861  cvmlift2lem12  35893  mvrsfpw  36085  elmsta  36127  msubvrs  36139  mclsind  36149  nepss  36297  dfon2lem4  36363  trer  36935  neiin  36951  neibastop1  36978  neibastop2lem  36979  topmeet  36983  filnetlem3  36999  weiunfr  37086  elttcirr  37150  bj-disj2r  37772  bj-restpw  37842  bj-restb  37844  bj-restuni2  37848  bj-ablsscmn  38030  topdifinffinlem  38101  opnmbllem0  38405  mblfinlem4  38409  mbfposadd  38416  heibor1lem  38559  heiborlem1  38561  heiborlem3  38563  heiborlem10  38570  opidonOLD  38602  disjimin  39599  lshpinN  39862  lcvexchlem1  39907  lcvexchlem5  39911  pmod1i  40721  pmodN  40723  osumcllem7N  40835  pexmidlem4N  40846  dochdmj1  42263  dochexmidlem4  42336  lcfrlem25  42440  mapd1o  42521  mapdin  42535  elrfi  43539  elrfirn  43540  fnwe2lem2  43892  aomclem2  43896  lsmfgcl  43915  lmhmfgima  43925  lmhmfgsplit  43927  lmhmlnmsplit  43928  hbt  43971  ofoafg  44195  trrelind  44505  iunrelexp0  44542  isotone2  44889  grumnudlem  45109  ismnushort  45125  onfrALTlem3  45367  onfrALTlem2  45369  onfrALTlem3VD  45709  onfrALTlem2VD  45711  iunconnlem2  45757  wfac8prim  45825  restuni6  45954  disjinfi  46024  inmap  46039  fsumiunss  46405  islptre  46449  sumnnodd  46460  limcresiooub  46470  limcresioolb  46471  limcleqr  46472  limclner  46479  limclr  46483  limsuplesup  46527  limsuppnfdlem  46529  limsupres  46533  liminfgord  46582  liminfgf  46586  liminfcl  46591  limsupresxr  46594  liminfresxr  46595  liminfval2  46596  liminflelimsuplem  46603  liminfvalxr  46611  icccncfext  46715  fourierdlem20  46955  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem76  47010  fourierdlem103  47037  fourierdlem104  47038  fourierdlem113  47047  fouriersw  47059  salgencntex  47171  sge0less  47220  sge0resplit  47234  sge0split  47237  sge0iunmptlemre  47243  sge0fodjrnlem  47244  caragencmpl  47363  ovolval2lem  47471  ovolval2  47472  ovolval3  47475  ovolval4lem2  47478  sssmf  47566  wrddrin  47715  chndrin  47720  chnrrin  47725  numtowerdt  47734  tmachlem-fssscan  47778  fcoreslem4  47954  fcoresf1  47957  fcoresfo  47959  3f1oss1  47963  rngchomrnghmresALTV  49194  termc  50445