Theorem inss2 4218

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

Syntax hints:   ∩ cin 3930   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-in 3938  df-ss 3948

This theorem is referenced by:  inindif  4355  difin0  4454  iunxdif3  5076  relin2  5797  relres  5997  idssxp  6041  ssrnres  6172  cnvrescnv  6189  ordin  6387  onfr  6396  ordelinel  6460  fnresin2  6669  fresaunres2  6755  ssimaex  6969  exfo  7100  ffvresb  7120  fnfvimad  7231  ofrfvalg  7684  ofval  7687  ofrval  7688  off  7694  ofres  7695  ofco  7701  fnwelem  8135  fnse  8137  fprlem1  8304  tfrlem5  8399  pmresg  8889  ixpfi2  9367  elfiun  9447  marypha1lem  9450  ordtypelem6  9542  ordtypelem7  9543  hartogslem1  9561  unxpwdom  9608  epfrs  9750  tcmin  9760  bnd2  9912  tskwe  9969  r0weon  10031  infxpenlem  10032  djuinf  10208  ackbij1lem9  10246  ackbij1lem10  10247  ackbij1lem15  10252  ackbij1lem16  10253  ackbij1b  10257  sdom2en01  10321  fin23lem26  10344  fin23lem13  10351  isfin1-3  10405  fin56  10412  fin1a2lem9  10427  brdom3  10547  brdom5  10548  brdom4  10549  fpwwe2lem11  10660  fpwwe2  10662  canthwelem  10669  gruima  10821  ingru  10834  gruina  10837  grur1a  10838  ltrelpi  10908  ltrelnq  10945  nqerf  10949  fzfi  13995  xptrrel  15004  rexanuz  15369  limsupgord  15493  limsupcl  15494  limsupgf  15496  limsupgle  15498  o1of2  15634  o1rlimmul  15640  ackbijnn  15849  bitsinv1  16466  bitsinvp1  16473  sadcaddlem  16481  sadadd2lem  16483  sadadd3  16485  sadaddlem  16490  sadasslem  16494  sadeq  16496  smupval  16512  prmrec  16947  structcnvcnv  17177  ressbasss  17265  ressbasssOLD  17266  ressress  17273  restsspw  17450  submre  17622  isacs1i  17674  rescabs  17851  resscat  17870  funcres2c  17921  ressffth  17958  catccatid  18124  catcisolem  18128  catciso  18129  yoniso  18302  acsinfd  18571  acsdomd  18572  tsrss  18604  idresefmnd  18882  idrespermg  19397  mvdco  19431  lsmmod  19661  rnghmresfn  20584  rnghmsscmap  20595  rhmresfn  20613  rhmsscmap  20624  rhmsubclem4  20653  acsfn1p  20764  lssacs  20929  lidlssbas  21179  zringlpirlem2  21429  zringlpirlem3  21430  asplss  21839  ressmplbas  21991  subrgmpl  21995  mplind  22033  ressply1bas  22169  pf1rcl  22292  ressply1evl  22313  evls1addd  22314  evls1muld  22315  evls1vsca  22316  evls1maprhm  22319  ofco2  22394  basdif0  22896  eltg4i  22903  ntrss2  23000  ntrin  23004  isopn3  23009  resttopon  23104  restuni2  23110  restcld  23115  restfpw  23122  neitr  23123  cnrest2r  23230  cnpresti  23231  cnprest  23232  lmss  23241  cnrmi  23303  restcnrm  23305  resthauslem  23306  imacmp  23340  fiuncmp  23347  subislly  23424  islly2  23427  cldllycmp  23438  hauspwdom  23444  kgeni  23480  llycmpkgen2  23493  ptbasfi  23524  ptclsg  23558  ptcnplem  23564  txtube  23583  txcmplem2  23585  txkgen  23595  kqdisj  23675  fbasrn  23827  trfg  23834  isufil2  23851  fmfnfmlem4  23900  hauspwpwf1  23930  txflf  23949  alexsubALTlem4  23993  tmdgsum2  24039  tsmsres  24087  tsmsxplem1  24096  ustexsym  24159  ustund  24165  trust  24173  utoptop  24178  restutop  24181  metrest  24468  restmetu  24514  tgioo  24740  reconnlem2  24772  cphsqrtcl  25141  tcphcph  25194  cfilresi  25252  caussi  25254  causs  25255  ovolfioo  25425  ovolficc  25426  ovolficcss  25427  ovolfsf  25429  ovollb  25437  ovolicc2lem1  25475  ovolicc2lem2  25476  ovolicc2lem3  25477  ovolicc2lem4  25478  ovolicc2  25480  nulmbl  25493  voliunlem1  25508  ovolfs2  25529  uniiccdif  25536  uniioovol  25537  uniiccvol  25538  uniioombllem2  25541  uniioombllem3a  25542  uniioombllem3  25543  uniioombllem4  25544  uniioombllem5  25545  uniioombllem6  25546  uniioombl  25547  dyadmbllem  25557  dyadmbl  25558  opnmbllem  25559  volcn  25564  volivth  25565  mbfadd  25619  mbfsub  25620  i1fima  25636  i1fima2  25637  i1fd  25639  i1fadd  25653  i1fmul  25654  itg1addlem2  25655  itg1addlem4  25657  itg1addlem5  25658  i1fres  25663  mbfmul  25684  bddmulibl  25797  ellimc2  25835  ellimc3  25837  limcflf  25839  limcresi  25843  limciun  25852  dvreslem  25867  dvres2lem  25868  dvres3a  25872  cpnres  25896  dvaddbr  25897  dvmulbr  25898  dvmulbrOLD  25899  dvmptres3  25917  lhop1lem  25975  rlimcnp2  26933  xrlimcnp  26935  chpchtsum  27187  2sqlem8  27394  2sqlem9  27395  rpvmasumlem  27455  rplogsum  27495  dirith2  27496  nosupbnd2  27685  axtgsegcon  28448  axtg5seg  28449  axtgbtwnid  28450  axtgpasch  28451  axtgcont1  28452  tglng  28530  chdmm1i  31463  chm0i  31476  ledii  31522  lejdii  31524  pjoml2i  31571  pjoml4i  31573  cmcmlem  31577  cmbr4i  31587  osumcori  31629  pjssmii  31667  mayete3i  31714  riesz4  32050  riesz1  32051  cnlnadjeu  32064  nmopadjlei  32074  pjclem1  32181  pjci  32186  mdbr3  32283  mdbr4  32284  dmdbr2  32289  dmdbr5  32294  ssmd2  32298  mdslj1i  32305  mdslj2i  32306  mdsl1i  32307  mdsl2bi  32309  mdslmd1lem1  32311  mdslmd1lem2  32312  mdslmd2i  32316  csmdsymi  32320  cvexchlem  32354  atomli  32368  atcvat4i  32383  difininv  32503  disjxpin  32574  imadifxp  32587  off2  32624  mptiffisupp  32675  indsumin  32844  indf1ofs  32848  resspos  32951  resstos  32952  submomnd  33083  suborng  33342  idlinsubrg  33451  ressply1invg  33587  evls1subd  33590  algextdeglem7  33762  algextdeglem8  33763  ordtrestNEW  33957  pnfneige0  33987  lmxrge0  33988  qqhnm  34026  qqhcn  34027  rrhre  34057  gsumesum  34095  esumlub  34096  esumcst  34099  esumpcvgval  34114  hasheuni  34121  esumcvg  34122  sigainb  34172  carsgclctunlem2  34356  sibfinima  34376  sibfof  34377  eulerpartlemelr  34394  eulerpartlemgh  34415  eulerpartlemgf  34416  eulerpartlemgs2  34417  eulerpartlemn  34418  probmeasb  34467  cndprob01  34472  hashreprin  34657  reprfi2  34660  breprexpnat  34671  hgt750lemd  34685  hgt750lema  34694  tgoldbachgtde  34697  tgoldbachgtda  34698  tgoldbachgt  34700  bnj1293  34852  connpconn  35262  iccllysconn  35277  cvmsss2  35301  cvmcov2  35302  cvmopnlem  35305  cvmliftmolem2  35309  cvmlift2lem12  35341  mvrsfpw  35533  elmsta  35575  msubvrs  35587  mclsind  35597  nepss  35740  dfon2lem4  35809  trer  36339  neiin  36355  neibastop1  36382  neibastop2lem  36383  topmeet  36387  filnetlem3  36403  weiunfr  36490  bj-disj2r  37051  bj-restpw  37115  bj-restb  37117  bj-restuni2  37121  bj-ablsscmn  37301  topdifinffinlem  37370  opnmbllem0  37685  mblfinlem4  37689  mbfposadd  37696  heibor1lem  37838  heiborlem1  37840  heiborlem3  37842  heiborlem10  37849  opidonOLD  37881  disjimin  38774  lshpinN  39012  lcvexchlem1  39057  lcvexchlem5  39061  pmod1i  39872  pmodN  39874  osumcllem7N  39986  pexmidlem4N  39997  dochdmj1  41414  dochexmidlem4  41487  lcfrlem25  41591  mapd1o  41672  mapdin  41686  elrfi  42692  elrfirn  42693  fnwe2lem2  43050  aomclem2  43054  lsmfgcl  43073  lmhmfgima  43083  lmhmfgsplit  43085  lmhmlnmsplit  43086  hbt  43129  ofoafg  43353  trrelind  43664  iunrelexp0  43701  isotone2  44048  grumnudlem  44284  ismnushort  44300  onfrALTlem3  44544  onfrALTlem2  44546  onfrALTlem3VD  44886  onfrALTlem2VD  44888  iunconnlem2  44934  wfac8prim  45002  restuni6  45126  disjinfi  45196  inmap  45213  fsumiunss  45584  islptre  45628  sumnnodd  45639  limcresiooub  45651  limcresioolb  45652  limcleqr  45653  limclner  45660  limclr  45664  limsuplesup  45708  limsuppnfdlem  45710  limsupres  45714  liminfgord  45763  liminfgf  45767  liminfcl  45772  limsupresxr  45775  liminfresxr  45776  liminfval2  45777  liminflelimsuplem  45784  liminfvalxr  45792  icccncfext  45896  fourierdlem20  46136  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem76  46191  fourierdlem103  46218  fourierdlem104  46219  fourierdlem113  46228  fouriersw  46240  salgencntex  46352  sge0less  46401  sge0resplit  46415  sge0split  46418  sge0iunmptlemre  46424  sge0fodjrnlem  46425  caragencmpl  46544  ovolval2lem  46652  ovolval2  46653  ovolval3  46656  ovolval4lem2  46659  sssmf  46747  fcoreslem4  47075  fcoresf1  47078  fcoresfo  47080  3f1oss1  47084  rngchomrnghmresALTV  48234  termc  49384