Theorem inss2 4133

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 4105	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4132	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3956	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

This proof depends on syntax axioms:   ⊆ wss 3896   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090

This theorem is used by:  inindif  4323  vvin  4358  difin0  4427  uniin  4890  iunxdif3  5054  relin2  5792  relresOLD  5998  idssxp  6043  rnin  6139  ssrnres  6172  cnvrescnv  6190  ordin  6396  onfr  6405  ordelinel  6469  fnresin2  6670  fresaunres2  6759  ssimaex  6975  exfo  7110  ffvresb  7131  fnfvimad  7244  ofrfvalg  7705  ofval  7708  ofrval  7709  off  7715  ofres  7716  ofco  7722  fnwelem  8149  fnwe2lem3  8153  fnse  8156  fprlem1  8325  tfrlem5  8394  pmresg  8905  ixpfi2  9346  elfiun  9429  marypha1lem  9432  ordtypelem6  9524  ordtypelem7  9525  hartogslem1  9543  unxpwdom  9590  epfrs  9739  tcmin  9747  bnd2  9963  tskwe  10038  r0weon  10098  infxpenlem  10099  djuinf  10274  ackbij1lem9  10312  ackbij1lem10  10313  ackbij1lem15  10318  ackbij1lem16  10319  ackbij1b  10323  sdom2en01  10387  fin23lem26  10410  fin23lem13  10417  isfin1-3  10471  fin56  10478  fin1a2lem9  10493  brdom3  10614  brdom5  10615  brdom4  10616  fpwwe2lem11  10733  fpwwe2  10735  canthwelem  10742  gruima  10894  ingru  10907  gruina  10910  grur1a  10911  ltrelpi  10981  ltrelnq  11018  nqerf  11022  fzfi  14122  xptrrel  15142  rexanuz  15522  limsupgord  15648  limsupcl  15649  limsupgf  15651  limsupgle  15653  o1of2  15789  o1rlimmul  15795  ackbijnn  16006  bitsinv1  16621  bitsinvp1  16628  sadcaddlem  16636  sadadd2lem  16638  sadadd3  16640  sadaddlem  16645  sadasslem  16649  sadeq  16651  smupval  16667  prmrec  17109  structcnvcnv  17340  ressbasss  17426  ressbasssOLD  17427  ressress  17434  restsspw  17611  submre  17784  isacs1i  17840  rescabs  18017  resscat  18036  funcres2c  18087  ressffth  18124  catccatid  18290  catcisolem  18294  catciso  18295  yoniso  18468  resspos  18612  resstos  18613  acsinfd  18739  acsdomd  18740  tsrss  18772  idresefmnd  19104  idrespermg  19634  mvdco  19668  lsmmod  19898  submomnd  20355  rnghmresfn  20880  rnghmsscmap  20891  rhmresfn  20909  rhmsscmap  20920  rhmsubclem4  20949  acsfn1p  21065  suborng  21142  lssacs  21251  lidlssbas  21501  zringlpirlem2  21778  zringlpirlem3  21779  asplss  22190  ressmplbas  22345  subrgmpl  22349  mplind  22388  ressply1bas  22555  pf1rcl  22676  ressply1evl  22697  evls1addd  22698  evls1muld  22699  evls1vsca  22700  evls1maprhm  22703  ofco2  22775  basdif0  23280  eltg4i  23287  ntrss2  23384  ntrin  23388  isopn3  23393  resttopon  23488  restuni2  23494  restcld  23499  restfpw  23506  neitr  23507  cnrest2r  23614  cnpresti  23615  cnprest  23616  lmss  23625  cnrmi  23687  restcnrm  23689  resthauslem  23690  imacmp  23724  fiuncmp  23731  subislly  23809  islly2  23812  cldllycmp  23823  hauspwdom  23829  kgeni  23865  llycmpkgen2  23878  ptbasfi  23909  ptclsg  23943  ptcnplem  23949  txtube  23968  txcmplem2  23970  txkgen  23980  kqdisj  24060  fbasrn  24212  trfg  24219  isufil2  24236  fmfnfmlem4  24285  hauspwpwf1  24315  txflf  24334  alexsubALTlem4  24378  tmdgsum2  24424  tsmsres  24472  tsmsxplem1  24481  ustexsym  24544  ustund  24550  trust  24557  utoptop  24562  restutop  24565  metrest  24852  restmetu  24898  tgioo  25124  reconnlem2  25156  cphsqrtcl  25514  tcphcph  25567  cfilresi  25625  caussi  25627  causs  25628  ovolfioo  25797  ovolficc  25798  ovolficcss  25799  ovolfsf  25801  ovollb  25809  ovolicc2lem1  25847  ovolicc2lem2  25848  ovolicc2lem3  25849  ovolicc2lem4  25850  ovolicc2  25852  nulmbl  25865  voliunlem1  25880  ovolfs2  25901  uniiccdif  25908  uniioovol  25909  uniiccvol  25910  uniioombllem2  25913  uniioombllem3a  25914  uniioombllem3  25915  uniioombllem4  25916  uniioombllem5  25917  uniioombllem6  25918  uniioombl  25919  dyadmbllem  25929  dyadmbl  25930  opnmbllem  25931  volcn  25936  volivth  25937  mbfadd  25991  mbfsub  25992  i1fima  26008  i1fima2  26009  i1fd  26011  i1fadd  26025  i1fmul  26026  itg1addlem2  26027  itg1addlem4  26029  itg1addlem5  26030  i1fres  26035  mbfmul  26056  bddmulibl  26168  ellimc2  26206  ellimc3  26208  limcflf  26210  limcresi  26214  limciun  26223  dvreslem  26238  dvres2lem  26239  dvres3a  26243  cpnres  26266  dvaddbr  26267  dvmulbr  26268  dvmptres3  26285  lhop1lem  26342  rlimcnp2  27303  xrlimcnp  27305  chpchtsum  27555  2sqlem8  27762  2sqlem9  27763  rpvmasumlem  27823  rplogsum  27863  dirith2  27864  nosupbnd2  28082  axtgsegcon  28935  axtg5seg  28936  axtgbtwnid  28937  axtgpasch  28938  axtgcont1  28939  tglng  29018  chdmm1i  32088  chm0i  32101  ledii  32147  lejdii  32149  pjoml2i  32196  pjoml4i  32198  cmcmlem  32202  cmbr4i  32212  osumcori  32254  pjssmii  32292  mayete3i  32339  riesz4  32675  riesz1  32676  cnlnadjeu  32689  nmopadjlei  32699  pjclem1  32806  pjci  32811  mdbr3  32908  mdbr4  32909  dmdbr2  32914  dmdbr5  32919  ssmd2  32923  mdslj1i  32930  mdslj2i  32931  mdsl1i  32932  mdsl2bi  32934  mdslmd1lem1  32936  mdslmd1lem2  32937  mdslmd2i  32941  csmdsymi  32945  cvexchlem  32979  atomli  32993  atcvat4i  33008  difininv  33164  disjxpin  33233  imadifxp  33246  off2  33286  mptiffisupp  33337  indsumin  33478  indf1ofs  33483  idlinsubrg  34031  ressply1invg  34151  evls1subd  34154  algextdeglem7  34405  algextdeglem8  34406  ordtrestNEW  34603  pnfneige0  34633  lmxrge0  34634  qqhnm  34672  qqhcn  34673  rrhre  34703  gsumesum  34741  esumlub  34742  esumcst  34745  esumpcvgval  34760  hasheuni  34767  esumcvg  34768  sigainb  34819  carsgclctunlem2  35001  sibfinima  35021  sibfof  35022  eulerpartlemelr  35039  eulerpartlemgh  35060  eulerpartlemgf  35061  eulerpartlemgs2  35062  eulerpartlemn  35063  probmeasb  35112  cndprob01  35117  hashreprin  35299  reprfi2  35302  breprexpnat  35313  hgt750lemd  35327  hgt750lema  35336  tgoldbachgtde  35339  tgoldbachgtda  35340  tgoldbachgt  35342  bnj1293  35496  weexenwe  35816  connpconn  36090  iccllysconn  36105  cvmsss2  36129  cvmcov2  36130  cvmopnlem  36133  cvmliftmolem2  36137  cvmlift2lem12  36169  mvrsfpw  36361  elmsta  36403  msubvrs  36415  mclsind  36425  nepss  36579  dfon2lem4  36644  trer  37200  neiin  37216  neibastop1  37243  neibastop2lem  37244  topmeet  37248  filnetlem3  37264  weiunfr  37351  elttcirr  37415  bj-disj2r  38037  bj-resss2  38059  bj-restpw  38121  bj-restb  38123  bj-restuni2  38127  bj-ablsscmn  38308  topdifinffinlem  38379  opnmbllem0  38683  mblfinlem4  38687  mbfposadd  38694  heibor1lem  38852  heiborlem1  38854  heiborlem3  38856  heiborlem10  38863  opidonOLD  38895  disjimin  39892  lshpinN  40155  lcvexchlem1  40200  lcvexchlem5  40204  pmod1i  41014  pmodN  41016  osumcllem7N  41128  pexmidlem4N  41139  dochdmj1  42556  dochexmidlem4  42629  lcfrlem25  42733  mapd1o  42814  mapdin  42828  elrfi  43814  elrfirn  43815  aomclem2  44166  lsmfgcl  44185  lmhmfgima  44195  lmhmfgsplit  44197  lmhmlnmsplit  44198  hbt  44241  ofoafg  44465  trrelind  44774  iunrelexp0  44811  isotone2  45158  grumnudlem  45378  ismnushort  45394  onfrALTlem3  45635  onfrALTlem2  45637  onfrALTlem3VD  45977  onfrALTlem2VD  45979  iunconnlem2  46025  wfac8prim  46100  restuni6  46245  disjinfi  46315  inmap  46330  fsumiunss  46695  islptre  46739  sumnnodd  46750  limcresiooub  46760  limcresioolb  46761  limcleqr  46762  limclner  46769  limclr  46773  limsuplesup  46817  limsuppnfdlem  46819  limsupres  46823  liminfgord  46872  liminfgf  46876  liminfcl  46881  limsupresxr  46884  liminfresxr  46885  liminfval2  46886  liminflelimsuplem  46893  liminfvalxr  46901  icccncfext  47005  fourierdlem20  47245  fourierdlem48  47272  fourierdlem49  47273  fourierdlem50  47274  fourierdlem76  47300  fourierdlem103  47327  fourierdlem104  47328  fourierdlem113  47337  fouriersw  47349  salgencntex  47461  sge0less  47510  sge0resplit  47524  sge0split  47527  sge0iunmptlemre  47533  sge0fodjrnlem  47534  caragencmpl  47653  ovolval2lem  47761  ovolval2  47762  ovolval3  47765  ovolval4lem2  47768  sssmf  47856  wrddrin  48005  chndrin  48010  chnrrin  48015  numtowerdt  48024  tmachlem-fssscan  48068  fcoreslem4  48244  fcoresf1  48247  fcoresfo  48249  3f1oss1  48253  rngchomrnghmresALTV  49484  termc  50762