Theorem inss2 4156

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

Syntax hints:   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  difin0  4380  iunxdif3  4980  relin2  5650  relres  5847  idssxp  5883  ssrnres  6002  cnvrescnv  6019  ordin  6189  onfr  6198  ordelinel  6257  fnresin2  6445  fresaunres2  6524  ssimaex  6723  exfo  6848  ffvresb  6865  fnfvimad  6974  ofrfval  7397  ofval  7398  ofrval  7399  off  7404  ofres  7405  ofco  7409  fnwelem  7808  fnse  7810  tfrlem5  7999  pmresg  8417  nnfi  8696  ixpfi2  8806  elfiun  8878  marypha1lem  8881  ordtypelem6  8971  ordtypelem7  8972  hartogslem1  8990  unxpwdom  9037  epfrs  9157  tcmin  9167  bnd2  9306  tskwe  9363  r0weon  9423  infxpenlem  9424  djuinf  9599  ackbij1lem9  9639  ackbij1lem10  9640  ackbij1lem15  9645  ackbij1lem16  9646  ackbij1b  9650  sdom2en01  9713  fin23lem26  9736  fin23lem13  9743  isfin1-3  9797  fin56  9804  fin1a2lem9  9819  brdom3  9939  brdom5  9940  brdom4  9941  fpwwe2lem12  10052  fpwwe2  10054  canthwelem  10061  gruima  10213  ingru  10226  gruina  10229  grur1a  10230  ltrelpi  10300  ltrelnq  10337  nqerf  10341  fzfi  13335  xptrrel  14331  rexanuz  14697  limsupgord  14821  limsupcl  14822  limsupgf  14824  limsupgle  14826  o1of2  14961  o1rlimmul  14967  ackbijnn  15175  bitsinv1  15781  bitsinvp1  15788  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  smupval  15827  prmrec  16248  structcnvcnv  16489  ressbasss  16548  ressress  16554  restsspw  16697  submre  16868  isacs1i  16920  rescabs  17095  resscat  17114  funcres2c  17163  ressffth  17200  catccatid  17354  catcisolem  17358  catciso  17359  yoniso  17527  acsinfd  17782  acsdomd  17783  tsrss  17825  idresefmnd  18056  idrespermg  18531  mvdco  18565  sylow2a  18736  lsmmod  18793  acsfn1p  19571  lssacs  19732  zringlpirlem2  20178  zringlpirlem3  20179  asplss  20560  ressmplbas  20696  subrgmpl  20700  mplind  20741  ressply1bas  20858  pf1rcl  20973  ofco2  21056  basdif0  21558  eltg4i  21565  ntrss2  21662  ntrin  21666  isopn3  21671  resttopon  21766  restuni2  21772  restcld  21777  restfpw  21784  neitr  21785  cnrest2r  21892  cnpresti  21893  cnprest  21894  lmss  21903  cnrmi  21965  restcnrm  21967  resthauslem  21968  imacmp  22002  fiuncmp  22009  subislly  22086  islly2  22089  cldllycmp  22100  hauspwdom  22106  kgeni  22142  llycmpkgen2  22155  ptbasfi  22186  ptclsg  22220  ptcnplem  22226  txtube  22245  txcmplem2  22247  txkgen  22257  kqdisj  22337  fbasrn  22489  trfg  22496  isufil2  22513  fmfnfmlem4  22562  hauspwpwf1  22592  txflf  22611  alexsubALTlem4  22655  tmdgsum2  22701  tsmsres  22749  tsmsxplem1  22758  ustexsym  22821  ustund  22827  trust  22835  utoptop  22840  restutop  22843  metrest  23131  restmetu  23177  tgioo  23401  reconnlem2  23432  cphsqrtcl  23789  tcphcph  23841  cfilresi  23899  caussi  23901  causs  23902  ovolfioo  24071  ovolficc  24072  ovolficcss  24073  ovolfsf  24075  ovollb  24083  ovolicc2lem1  24121  ovolicc2lem2  24122  ovolicc2lem3  24123  ovolicc2lem4  24124  ovolicc2  24126  nulmbl  24139  voliunlem1  24154  ovolfs2  24175  uniiccdif  24182  uniioovol  24183  uniiccvol  24184  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem5  24191  uniioombllem6  24192  uniioombl  24193  dyadmbllem  24203  dyadmbl  24204  opnmbllem  24205  volcn  24210  volivth  24211  mbfadd  24265  mbfsub  24266  i1fima  24282  i1fima2  24283  i1fd  24285  i1fadd  24299  i1fmul  24300  itg1addlem2  24301  itg1addlem4  24303  itg1addlem5  24304  i1fres  24309  mbfmul  24330  bddmulibl  24442  ellimc2  24480  ellimc3  24482  limcflf  24484  limcresi  24488  limciun  24497  dvreslem  24512  dvres2lem  24513  dvres3a  24517  cpnres  24540  dvaddbr  24541  dvmulbr  24542  dvmptres3  24559  lhop1lem  24616  rlimcnp2  25552  xrlimcnp  25554  chpchtsum  25803  2sqlem8  26010  2sqlem9  26011  rpvmasumlem  26071  rplogsum  26111  dirith2  26112  axtgsegcon  26258  axtg5seg  26259  axtgbtwnid  26260  axtgpasch  26261  axtgcont1  26262  tglng  26340  chdmm1i  29260  chm0i  29273  ledii  29319  lejdii  29321  pjoml2i  29368  pjoml4i  29370  cmcmlem  29374  cmbr4i  29384  osumcori  29426  pjssmii  29464  mayete3i  29511  riesz4  29847  riesz1  29848  cnlnadjeu  29861  nmopadjlei  29871  pjclem1  29978  pjci  29983  mdbr3  30080  mdbr4  30081  dmdbr2  30086  dmdbr5  30091  ssmd2  30095  mdslj1i  30102  mdslj2i  30103  mdsl1i  30104  mdsl2bi  30106  mdslmd1lem1  30108  mdslmd1lem2  30109  mdslmd2i  30113  csmdsymi  30117  cvexchlem  30151  atomli  30165  atcvat4i  30180  inindif  30287  difininv  30288  disjxpin  30351  imadifxp  30364  off2  30402  resspos  30672  resstos  30673  submomnd  30761  suborng  30939  idlinsubrg  31016  ordtrestNEW  31274  pnfneige0  31304  lmxrge0  31305  qqhnm  31341  qqhcn  31342  rrhre  31372  indsumin  31391  indf1ofs  31395  gsumesum  31428  esumlub  31429  esumcst  31432  esumpcvgval  31447  hasheuni  31454  esumcvg  31455  sigainb  31505  carsgclctunlem2  31687  sibfinima  31707  sibfof  31708  eulerpartlemelr  31725  eulerpartlemgh  31746  eulerpartlemgf  31747  eulerpartlemgs2  31748  eulerpartlemn  31749  probmeasb  31798  cndprob01  31803  hashreprin  32001  reprfi2  32004  breprexpnat  32015  hgt750lemd  32029  hgt750lema  32038  tgoldbachgtde  32041  tgoldbachgtda  32042  tgoldbachgt  32044  bnj1293  32198  connpconn  32595  iccllysconn  32610  cvmsss2  32634  cvmcov2  32635  cvmopnlem  32638  cvmliftmolem2  32642  cvmlift2lem12  32674  mvrsfpw  32866  elmsta  32908  msubvrs  32920  mclsind  32930  nepss  33061  dfon2lem4  33144  fprlem1  33250  nosupbnd2  33329  trer  33777  neiin  33793  neibastop1  33820  neibastop2lem  33821  topmeet  33825  filnetlem3  33841  bj-disj2r  34464  bj-restpw  34507  bj-restb  34509  bj-restuni2  34513  bj-ablsscmn  34693  topdifinffinlem  34764  opnmbllem0  35093  mblfinlem4  35097  mbfposadd  35104  heibor1lem  35247  heiborlem1  35249  heiborlem3  35251  heiborlem10  35258  opidonOLD  35290  disjimin  36141  lshpinN  36285  lcvexchlem1  36330  lcvexchlem5  36334  pmod1i  37144  pmodN  37146  osumcllem7N  37258  pexmidlem4N  37269  dochdmj1  38686  dochexmidlem4  38759  lcfrlem25  38863  mapd1o  38944  mapdin  38958  elrfi  39635  elrfirn  39636  fnwe2lem2  39995  aomclem2  39999  lsmfgcl  40018  lmhmfgima  40028  lmhmfgsplit  40030  lmhmlnmsplit  40031  hbt  40074  trrelind  40366  iunrelexp0  40403  isotone2  40752  grumnudlem  40993  onfrALTlem3  41250  onfrALTlem2  41252  onfrALTlem3VD  41593  onfrALTlem2VD  41595  iunconnlem2  41641  restuni6  41757  disjinfi  41820  inmap  41838  dmresss  41867  fsumiunss  42217  islptre  42261  sumnnodd  42272  limcresiooub  42284  limcresioolb  42285  limcleqr  42286  limclner  42293  limclr  42297  limsuplesup  42341  limsuppnfdlem  42343  limsupres  42347  liminfgord  42396  liminfgf  42400  liminfcl  42405  limsupresxr  42408  liminfresxr  42409  liminfval2  42410  liminflelimsuplem  42417  liminfvalxr  42425  icccncfext  42529  fourierdlem20  42769  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem76  42824  fourierdlem103  42851  fourierdlem104  42852  fourierdlem113  42861  fouriersw  42873  salgencntex  42983  sge0less  43031  sge0resplit  43045  sge0split  43048  sge0iunmptlemre  43054  sge0fodjrnlem  43055  caragencmpl  43174  ovolval2lem  43282  ovolval2  43283  ovolval3  43286  ovolval4lem2  43289  sssmf  43372  lidlssbas  44546  rnghmresfn  44587  rnghmsscmap  44598  rngchomrnghmresALTV  44620  rhmresfn  44633  rhmsscmap  44644  rhmsubclem4  44713