Theorem inss2 4220

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 4191	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4219	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 4013	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3932   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-in 3940  df-ss 3950

This theorem is referenced by:  inindif  4357  difin0  4456  iunxdif3  5077  relin2  5805  relres  6005  idssxp  6049  ssrnres  6180  cnvrescnv  6197  ordin  6395  onfr  6404  ordelinel  6466  fnresin2  6675  fresaunres2  6761  ssimaex  6975  exfo  7106  ffvresb  7126  fnfvimad  7237  ofrfvalg  7688  ofval  7691  ofrval  7692  off  7698  ofres  7699  ofco  7705  fnwelem  8139  fnse  8141  fprlem1  8308  tfrlem5  8403  pmresg  8893  ixpfi2  9373  elfiun  9453  marypha1lem  9456  ordtypelem6  9546  ordtypelem7  9547  hartogslem1  9565  unxpwdom  9612  epfrs  9754  tcmin  9764  bnd2  9916  tskwe  9973  r0weon  10035  infxpenlem  10036  djuinf  10212  ackbij1lem9  10250  ackbij1lem10  10251  ackbij1lem15  10256  ackbij1lem16  10257  ackbij1b  10261  sdom2en01  10325  fin23lem26  10348  fin23lem13  10355  isfin1-3  10409  fin56  10416  fin1a2lem9  10431  brdom3  10551  brdom5  10552  brdom4  10553  fpwwe2lem11  10664  fpwwe2  10666  canthwelem  10673  gruima  10825  ingru  10838  gruina  10841  grur1a  10842  ltrelpi  10912  ltrelnq  10949  nqerf  10953  fzfi  13996  xptrrel  15002  rexanuz  15367  limsupgord  15491  limsupcl  15492  limsupgf  15494  limsupgle  15496  o1of2  15632  o1rlimmul  15638  ackbijnn  15847  bitsinv1  16462  bitsinvp1  16469  sadcaddlem  16477  sadadd2lem  16479  sadadd3  16481  sadaddlem  16486  sadasslem  16490  sadeq  16492  smupval  16508  prmrec  16943  structcnvcnv  17173  ressbasss  17266  ressbasssOLD  17267  ressress  17274  restsspw  17452  submre  17624  isacs1i  17676  rescabs  17853  rescabsOLD  17854  resscat  17873  funcres2c  17924  ressffth  17961  catccatid  18127  catcisolem  18131  catciso  18132  yoniso  18305  acsinfd  18575  acsdomd  18576  tsrss  18608  idresefmnd  18886  idrespermg  19402  mvdco  19436  lsmmod  19666  rnghmresfn  20592  rnghmsscmap  20603  rhmresfn  20621  rhmsscmap  20632  rhmsubclem4  20661  acsfn1p  20773  lssacs  20938  lidlssbas  21190  zringlpirlem2  21441  zringlpirlem3  21442  asplss  21861  ressmplbas  22013  subrgmpl  22017  mplind  22061  ressply1bas  22197  pf1rcl  22320  ressply1evl  22341  evls1addd  22342  evls1muld  22343  evls1vsca  22344  evls1maprhm  22347  ofco2  22424  basdif0  22926  eltg4i  22933  ntrss2  23030  ntrin  23034  isopn3  23039  resttopon  23134  restuni2  23140  restcld  23145  restfpw  23152  neitr  23153  cnrest2r  23260  cnpresti  23261  cnprest  23262  lmss  23271  cnrmi  23333  restcnrm  23335  resthauslem  23336  imacmp  23370  fiuncmp  23377  subislly  23454  islly2  23457  cldllycmp  23468  hauspwdom  23474  kgeni  23510  llycmpkgen2  23523  ptbasfi  23554  ptclsg  23588  ptcnplem  23594  txtube  23613  txcmplem2  23615  txkgen  23625  kqdisj  23705  fbasrn  23857  trfg  23864  isufil2  23881  fmfnfmlem4  23930  hauspwpwf1  23960  txflf  23979  alexsubALTlem4  24023  tmdgsum2  24069  tsmsres  24117  tsmsxplem1  24126  ustexsym  24189  ustund  24195  trust  24203  utoptop  24208  restutop  24211  metrest  24500  restmetu  24546  tgioo  24772  reconnlem2  24804  cphsqrtcl  25173  tcphcph  25226  cfilresi  25284  caussi  25286  causs  25287  ovolfioo  25457  ovolficc  25458  ovolficcss  25459  ovolfsf  25461  ovollb  25469  ovolicc2lem1  25507  ovolicc2lem2  25508  ovolicc2lem3  25509  ovolicc2lem4  25510  ovolicc2  25512  nulmbl  25525  voliunlem1  25540  ovolfs2  25561  uniiccdif  25568  uniioovol  25569  uniiccvol  25570  uniioombllem2  25573  uniioombllem3a  25574  uniioombllem3  25575  uniioombllem4  25576  uniioombllem5  25577  uniioombllem6  25578  uniioombl  25579  dyadmbllem  25589  dyadmbl  25590  opnmbllem  25591  volcn  25596  volivth  25597  mbfadd  25651  mbfsub  25652  i1fima  25668  i1fima2  25669  i1fd  25671  i1fadd  25685  i1fmul  25686  itg1addlem2  25687  itg1addlem4  25689  itg1addlem5  25690  i1fres  25695  mbfmul  25716  bddmulibl  25829  ellimc2  25867  ellimc3  25869  limcflf  25871  limcresi  25875  limciun  25884  dvreslem  25899  dvres2lem  25900  dvres3a  25904  cpnres  25928  dvaddbr  25929  dvmulbr  25930  dvmulbrOLD  25931  dvmptres3  25949  lhop1lem  26007  rlimcnp2  26964  xrlimcnp  26966  chpchtsum  27218  2sqlem8  27425  2sqlem9  27426  rpvmasumlem  27486  rplogsum  27526  dirith2  27527  nosupbnd2  27716  axtgsegcon  28427  axtg5seg  28428  axtgbtwnid  28429  axtgpasch  28430  axtgcont1  28431  tglng  28509  chdmm1i  31443  chm0i  31456  ledii  31502  lejdii  31504  pjoml2i  31551  pjoml4i  31553  cmcmlem  31557  cmbr4i  31567  osumcori  31609  pjssmii  31647  mayete3i  31694  riesz4  32030  riesz1  32031  cnlnadjeu  32044  nmopadjlei  32054  pjclem1  32161  pjci  32166  mdbr3  32263  mdbr4  32264  dmdbr2  32269  dmdbr5  32274  ssmd2  32278  mdslj1i  32285  mdslj2i  32286  mdsl1i  32287  mdsl2bi  32289  mdslmd1lem1  32291  mdslmd1lem2  32292  mdslmd2i  32296  csmdsymi  32300  cvexchlem  32334  atomli  32348  atcvat4i  32363  difininv  32483  disjxpin  32548  imadifxp  32561  off2  32598  mptiffisupp  32649  indsumin  32794  indf1ofs  32798  resspos  32902  resstos  32903  submomnd  33033  suborng  33291  idlinsubrg  33400  ressply1invg  33535  evls1subd  33538  algextdeglem7  33705  algextdeglem8  33706  ordtrestNEW  33861  pnfneige0  33891  lmxrge0  33892  qqhnm  33932  qqhcn  33933  rrhre  33963  gsumesum  34001  esumlub  34002  esumcst  34005  esumpcvgval  34020  hasheuni  34027  esumcvg  34028  sigainb  34078  carsgclctunlem2  34262  sibfinima  34282  sibfof  34283  eulerpartlemelr  34300  eulerpartlemgh  34321  eulerpartlemgf  34322  eulerpartlemgs2  34323  eulerpartlemn  34324  probmeasb  34373  cndprob01  34378  hashreprin  34576  reprfi2  34579  breprexpnat  34590  hgt750lemd  34604  hgt750lema  34613  tgoldbachgtde  34616  tgoldbachgtda  34617  tgoldbachgt  34619  bnj1293  34771  connpconn  35181  iccllysconn  35196  cvmsss2  35220  cvmcov2  35221  cvmopnlem  35224  cvmliftmolem2  35228  cvmlift2lem12  35260  mvrsfpw  35452  elmsta  35494  msubvrs  35506  mclsind  35516  nepss  35659  dfon2lem4  35728  trer  36258  neiin  36274  neibastop1  36301  neibastop2lem  36302  topmeet  36306  filnetlem3  36322  weiunfr  36409  bj-disj2r  36970  bj-restpw  37034  bj-restb  37036  bj-restuni2  37040  bj-ablsscmn  37220  topdifinffinlem  37289  opnmbllem0  37604  mblfinlem4  37608  mbfposadd  37615  heibor1lem  37757  heiborlem1  37759  heiborlem3  37761  heiborlem10  37768  opidonOLD  37800  disjimin  38693  lshpinN  38931  lcvexchlem1  38976  lcvexchlem5  38980  pmod1i  39791  pmodN  39793  osumcllem7N  39905  pexmidlem4N  39916  dochdmj1  41333  dochexmidlem4  41406  lcfrlem25  41510  mapd1o  41591  mapdin  41605  elrfi  42650  elrfirn  42651  fnwe2lem2  43008  aomclem2  43012  lsmfgcl  43031  lmhmfgima  43041  lmhmfgsplit  43043  lmhmlnmsplit  43044  hbt  43087  ofoafg  43312  trrelind  43623  iunrelexp0  43660  isotone2  44007  grumnudlem  44249  ismnushort  44265  onfrALTlem3  44509  onfrALTlem2  44511  onfrALTlem3VD  44852  onfrALTlem2VD  44854  iunconnlem2  44900  wfac8prim  44964  restuni6  45072  disjinfi  45142  inmap  45159  fsumiunss  45535  islptre  45579  sumnnodd  45590  limcresiooub  45602  limcresioolb  45603  limcleqr  45604  limclner  45611  limclr  45615  limsuplesup  45659  limsuppnfdlem  45661  limsupres  45665  liminfgord  45714  liminfgf  45718  liminfcl  45723  limsupresxr  45726  liminfresxr  45727  liminfval2  45728  liminflelimsuplem  45735  liminfvalxr  45743  icccncfext  45847  fourierdlem20  46087  fourierdlem48  46114  fourierdlem49  46115  fourierdlem50  46116  fourierdlem76  46142  fourierdlem103  46169  fourierdlem104  46170  fourierdlem113  46179  fouriersw  46191  salgencntex  46303  sge0less  46352  sge0resplit  46366  sge0split  46369  sge0iunmptlemre  46375  sge0fodjrnlem  46376  caragencmpl  46495  ovolval2lem  46603  ovolval2  46604  ovolval3  46607  ovolval4lem2  46610  sssmf  46698  fcoreslem4  47024  fcoresf1  47027  fcoresfo  47029  3f1oss1  47033  rngchomrnghmresALTV  48141  termc  49118