Theorem inss2 4163

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

Syntax hints:   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  difin0  4407  iunxdif3  5024  relin2  5723  relres  5920  idssxp  5956  ssrnres  6081  cnvrescnv  6098  ordin  6296  onfr  6305  ordelinel  6364  fnresin2  6558  fresaunres2  6646  ssimaex  6853  exfo  6981  ffvresb  6998  fnfvimad  7110  ofrfvalg  7541  ofval  7544  ofrval  7545  off  7551  ofres  7552  ofco  7556  fnwelem  7972  fnse  7974  fprlem1  8116  tfrlem5  8211  pmresg  8658  nnfiOLD  9015  ixpfi2  9117  elfiun  9189  marypha1lem  9192  ordtypelem6  9282  ordtypelem7  9283  hartogslem1  9301  unxpwdom  9348  epfrs  9489  tcmin  9499  bnd2  9651  tskwe  9708  r0weon  9768  infxpenlem  9769  djuinf  9944  ackbij1lem9  9984  ackbij1lem10  9985  ackbij1lem15  9990  ackbij1lem16  9991  ackbij1b  9995  sdom2en01  10058  fin23lem26  10081  fin23lem13  10088  isfin1-3  10142  fin56  10149  fin1a2lem9  10164  brdom3  10284  brdom5  10285  brdom4  10286  fpwwe2lem11  10397  fpwwe2  10399  canthwelem  10406  gruima  10558  ingru  10571  gruina  10574  grur1a  10575  ltrelpi  10645  ltrelnq  10682  nqerf  10686  fzfi  13692  xptrrel  14691  rexanuz  15057  limsupgord  15181  limsupcl  15182  limsupgf  15184  limsupgle  15186  o1of2  15322  o1rlimmul  15328  ackbijnn  15540  bitsinv1  16149  bitsinvp1  16156  sadcaddlem  16164  sadadd2lem  16166  sadadd3  16168  sadaddlem  16173  sadasslem  16177  sadeq  16179  smupval  16195  prmrec  16623  structcnvcnv  16854  ressbasss  16950  ressress  16958  restsspw  17142  submre  17314  isacs1i  17366  rescabs  17547  rescabsOLD  17548  resscat  17567  funcres2c  17617  ressffth  17654  catccatid  17821  catcisolem  17825  catciso  17826  yoniso  18003  acsinfd  18274  acsdomd  18275  tsrss  18307  idresefmnd  18538  idrespermg  19019  mvdco  19053  lsmmod  19281  acsfn1p  20067  lssacs  20229  zringlpirlem2  20685  zringlpirlem3  20686  asplss  21078  ressmplbas  21229  subrgmpl  21233  mplind  21278  ressply1bas  21400  pf1rcl  21515  ofco2  21600  basdif0  22103  eltg4i  22110  ntrss2  22208  ntrin  22212  isopn3  22217  resttopon  22312  restuni2  22318  restcld  22323  restfpw  22330  neitr  22331  cnrest2r  22438  cnpresti  22439  cnprest  22440  lmss  22449  cnrmi  22511  restcnrm  22513  resthauslem  22514  imacmp  22548  fiuncmp  22555  subislly  22632  islly2  22635  cldllycmp  22646  hauspwdom  22652  kgeni  22688  llycmpkgen2  22701  ptbasfi  22732  ptclsg  22766  ptcnplem  22772  txtube  22791  txcmplem2  22793  txkgen  22803  kqdisj  22883  fbasrn  23035  trfg  23042  isufil2  23059  fmfnfmlem4  23108  hauspwpwf1  23138  txflf  23157  alexsubALTlem4  23201  tmdgsum2  23247  tsmsres  23295  tsmsxplem1  23304  ustexsym  23367  ustund  23373  trust  23381  utoptop  23386  restutop  23389  metrest  23680  restmetu  23726  tgioo  23959  reconnlem2  23990  cphsqrtcl  24348  tcphcph  24401  cfilresi  24459  caussi  24461  causs  24462  ovolfioo  24631  ovolficc  24632  ovolficcss  24633  ovolfsf  24635  ovollb  24643  ovolicc2lem1  24681  ovolicc2lem2  24682  ovolicc2lem3  24683  ovolicc2lem4  24684  ovolicc2  24686  nulmbl  24699  voliunlem1  24714  ovolfs2  24735  uniiccdif  24742  uniioovol  24743  uniiccvol  24744  uniioombllem2  24747  uniioombllem3a  24748  uniioombllem3  24749  uniioombllem4  24750  uniioombllem5  24751  uniioombllem6  24752  uniioombl  24753  dyadmbllem  24763  dyadmbl  24764  opnmbllem  24765  volcn  24770  volivth  24771  mbfadd  24825  mbfsub  24826  i1fima  24842  i1fima2  24843  i1fd  24845  i1fadd  24859  i1fmul  24860  itg1addlem2  24861  itg1addlem4  24863  itg1addlem4OLD  24864  itg1addlem5  24865  i1fres  24870  mbfmul  24891  bddmulibl  25003  ellimc2  25041  ellimc3  25043  limcflf  25045  limcresi  25049  limciun  25058  dvreslem  25073  dvres2lem  25074  dvres3a  25078  cpnres  25101  dvaddbr  25102  dvmulbr  25103  dvmptres3  25120  lhop1lem  25177  rlimcnp2  26116  xrlimcnp  26118  chpchtsum  26367  2sqlem8  26574  2sqlem9  26575  rpvmasumlem  26635  rplogsum  26675  dirith2  26676  axtgsegcon  26825  axtg5seg  26826  axtgbtwnid  26827  axtgpasch  26828  axtgcont1  26829  tglng  26907  chdmm1i  29839  chm0i  29852  ledii  29898  lejdii  29900  pjoml2i  29947  pjoml4i  29949  cmcmlem  29953  cmbr4i  29963  osumcori  30005  pjssmii  30043  mayete3i  30090  riesz4  30426  riesz1  30427  cnlnadjeu  30440  nmopadjlei  30450  pjclem1  30557  pjci  30562  mdbr3  30659  mdbr4  30660  dmdbr2  30665  dmdbr5  30670  ssmd2  30674  mdslj1i  30681  mdslj2i  30682  mdsl1i  30683  mdsl2bi  30685  mdslmd1lem1  30687  mdslmd1lem2  30688  mdslmd2i  30692  csmdsymi  30696  cvexchlem  30730  atomli  30744  atcvat4i  30759  inindif  30863  difininv  30864  disjxpin  30927  imadifxp  30940  off2  30978  resspos  31244  resstos  31245  submomnd  31336  suborng  31514  idlinsubrg  31608  ordtrestNEW  31871  pnfneige0  31901  lmxrge0  31902  qqhnm  31940  qqhcn  31941  rrhre  31971  indsumin  31990  indf1ofs  31994  gsumesum  32027  esumlub  32028  esumcst  32031  esumpcvgval  32046  hasheuni  32053  esumcvg  32054  sigainb  32104  carsgclctunlem2  32286  sibfinima  32306  sibfof  32307  eulerpartlemelr  32324  eulerpartlemgh  32345  eulerpartlemgf  32346  eulerpartlemgs2  32347  eulerpartlemn  32348  probmeasb  32397  cndprob01  32402  hashreprin  32600  reprfi2  32603  breprexpnat  32614  hgt750lemd  32628  hgt750lema  32637  tgoldbachgtde  32640  tgoldbachgtda  32641  tgoldbachgt  32643  bnj1293  32796  connpconn  33197  iccllysconn  33212  cvmsss2  33236  cvmcov2  33237  cvmopnlem  33240  cvmliftmolem2  33244  cvmlift2lem12  33276  mvrsfpw  33468  elmsta  33510  msubvrs  33522  mclsind  33532  nepss  33662  dfon2lem4  33762  nosupbnd2  33919  trer  34505  neiin  34521  neibastop1  34548  neibastop2lem  34549  topmeet  34553  filnetlem3  34569  bj-disj2r  35218  bj-restpw  35263  bj-restb  35265  bj-restuni2  35269  bj-ablsscmn  35449  topdifinffinlem  35518  opnmbllem0  35813  mblfinlem4  35817  mbfposadd  35824  heibor1lem  35967  heiborlem1  35969  heiborlem3  35971  heiborlem10  35978  opidonOLD  36010  disjimin  36859  lshpinN  37003  lcvexchlem1  37048  lcvexchlem5  37052  pmod1i  37862  pmodN  37864  osumcllem7N  37976  pexmidlem4N  37987  dochdmj1  39404  dochexmidlem4  39477  lcfrlem25  39581  mapd1o  39662  mapdin  39676  elrfi  40516  elrfirn  40517  fnwe2lem2  40876  aomclem2  40880  lsmfgcl  40899  lmhmfgima  40909  lmhmfgsplit  40911  lmhmlnmsplit  40912  hbt  40955  trrelind  41273  iunrelexp0  41310  isotone2  41659  grumnudlem  41903  ismnushort  41919  onfrALTlem3  42164  onfrALTlem2  42166  onfrALTlem3VD  42507  onfrALTlem2VD  42509  iunconnlem2  42555  restuni6  42671  disjinfi  42731  inmap  42749  dmresss  42774  fsumiunss  43116  islptre  43160  sumnnodd  43171  limcresiooub  43183  limcresioolb  43184  limcleqr  43185  limclner  43192  limclr  43196  limsuplesup  43240  limsuppnfdlem  43242  limsupres  43246  liminfgord  43295  liminfgf  43299  liminfcl  43304  limsupresxr  43307  liminfresxr  43308  liminfval2  43309  liminflelimsuplem  43316  liminfvalxr  43324  icccncfext  43428  fourierdlem20  43668  fourierdlem48  43695  fourierdlem49  43696  fourierdlem50  43697  fourierdlem76  43723  fourierdlem103  43750  fourierdlem104  43751  fourierdlem113  43760  fouriersw  43772  salgencntex  43882  sge0less  43930  sge0resplit  43944  sge0split  43947  sge0iunmptlemre  43953  sge0fodjrnlem  43954  caragencmpl  44073  ovolval2lem  44181  ovolval2  44182  ovolval3  44185  ovolval4lem2  44188  sssmf  44274  fcoreslem4  44560  fcoresf1  44563  fcoresfo  44565  lidlssbas  45480  rnghmresfn  45521  rnghmsscmap  45532  rngchomrnghmresALTV  45554  rhmresfn  45567  rhmsscmap  45578  rhmsubclem4  45647