Theorem inss2 4198

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 4170	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4197	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3992	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3912   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930

This theorem is referenced by:  inindif  4337  difin0  4437  uniin  4897  iunxdif3  5062  relin2  5798  relres  6002  idssxp  6049  rnin  6141  ssrnres  6175  cnvrescnv  6193  ordin  6388  onfr  6397  ordelinel  6461  fnresin2  6659  fresaunres2  6748  ssimaex  6964  exfo  7098  ffvresb  7119  fnfvimad  7230  ofrfvalg  7680  ofval  7683  ofrval  7684  off  7690  ofres  7691  ofco  7697  fnwelem  8123  fnse  8125  fprlem1  8293  tfrlem5  8362  pmresg  8864  ixpfi2  9303  elfiun  9386  marypha1lem  9389  ordtypelem6  9481  ordtypelem7  9482  hartogslem1  9500  unxpwdom  9547  epfrs  9696  tcmin  9704  bnd2  9875  tskwe  9932  r0weon  9992  infxpenlem  9993  djuinf  10168  ackbij1lem9  10206  ackbij1lem10  10207  ackbij1lem15  10212  ackbij1lem16  10213  ackbij1b  10217  sdom2en01  10282  fin23lem26  10305  fin23lem13  10312  isfin1-3  10366  fin56  10373  fin1a2lem9  10388  brdom3  10508  brdom5  10509  brdom4  10510  fpwwe2lem11  10622  fpwwe2  10624  canthwelem  10631  gruima  10783  ingru  10796  gruina  10799  grur1a  10800  ltrelpi  10870  ltrelnq  10907  nqerf  10911  fzfi  14004  xptrrel  15013  rexanuz  15393  limsupgord  15519  limsupcl  15520  limsupgf  15522  limsupgle  15524  o1of2  15660  o1rlimmul  15666  ackbijnn  15878  bitsinv1  16496  bitsinvp1  16503  sadcaddlem  16511  sadadd2lem  16513  sadadd3  16515  sadaddlem  16520  sadasslem  16524  sadeq  16526  smupval  16542  prmrec  16978  structcnvcnv  17209  ressbasss  17295  ressbasssOLD  17296  ressress  17303  restsspw  17480  submre  17653  isacs1i  17709  rescabs  17886  resscat  17905  funcres2c  17956  ressffth  17993  catccatid  18159  catcisolem  18163  catciso  18164  yoniso  18337  resspos  18481  resstos  18482  acsinfd  18608  acsdomd  18609  tsrss  18641  idresefmnd  18954  idrespermg  19477  mvdco  19511  lsmmod  19741  submomnd  20198  rnghmresfn  20700  rnghmsscmap  20711  rhmresfn  20729  rhmsscmap  20740  rhmsubclem4  20769  acsfn1p  20876  suborng  20953  lssacs  21062  lidlssbas  21312  zringlpirlem2  21578  zringlpirlem3  21579  asplss  21988  ressmplbas  22143  subrgmpl  22147  mplind  22186  ressply1bas  22353  pf1rcl  22474  ressply1evl  22495  evls1addd  22496  evls1muld  22497  evls1vsca  22498  evls1maprhm  22501  ofco2  22573  basdif0  23075  eltg4i  23082  ntrss2  23179  ntrin  23183  isopn3  23188  resttopon  23283  restuni2  23289  restcld  23294  restfpw  23301  neitr  23302  cnrest2r  23409  cnpresti  23410  cnprest  23411  lmss  23420  cnrmi  23482  restcnrm  23484  resthauslem  23485  imacmp  23519  fiuncmp  23526  subislly  23603  islly2  23606  cldllycmp  23617  hauspwdom  23623  kgeni  23659  llycmpkgen2  23672  ptbasfi  23703  ptclsg  23737  ptcnplem  23743  txtube  23762  txcmplem2  23764  txkgen  23774  kqdisj  23854  fbasrn  24006  trfg  24013  isufil2  24030  fmfnfmlem4  24079  hauspwpwf1  24109  txflf  24128  alexsubALTlem4  24172  tmdgsum2  24218  tsmsres  24266  tsmsxplem1  24275  ustexsym  24338  ustund  24344  trust  24351  utoptop  24356  restutop  24359  metrest  24646  restmetu  24692  tgioo  24918  reconnlem2  24950  cphsqrtcl  25308  tcphcph  25361  cfilresi  25419  caussi  25421  causs  25422  ovolfioo  25591  ovolficc  25592  ovolficcss  25593  ovolfsf  25595  ovollb  25603  ovolicc2lem1  25641  ovolicc2lem2  25642  ovolicc2lem3  25643  ovolicc2lem4  25644  ovolicc2  25646  nulmbl  25659  voliunlem1  25674  ovolfs2  25695  uniiccdif  25702  uniioovol  25703  uniiccvol  25704  uniioombllem2  25707  uniioombllem3a  25708  uniioombllem3  25709  uniioombllem4  25710  uniioombllem5  25711  uniioombllem6  25712  uniioombl  25713  dyadmbllem  25723  dyadmbl  25724  opnmbllem  25725  volcn  25730  volivth  25731  mbfadd  25785  mbfsub  25786  i1fima  25802  i1fima2  25803  i1fd  25805  i1fadd  25819  i1fmul  25820  itg1addlem2  25821  itg1addlem4  25823  itg1addlem5  25824  i1fres  25829  mbfmul  25850  bddmulibl  25963  ellimc2  26001  ellimc3  26003  limcflf  26005  limcresi  26009  limciun  26018  dvreslem  26033  dvres2lem  26034  dvres3a  26038  cpnres  26061  dvaddbr  26062  dvmulbr  26063  dvmptres3  26080  lhop1lem  26137  rlimcnp2  27093  xrlimcnp  27095  chpchtsum  27345  2sqlem8  27552  2sqlem9  27553  rpvmasumlem  27613  rplogsum  27653  dirith2  27654  nosupbnd2  27842  axtgsegcon  28695  axtg5seg  28696  axtgbtwnid  28697  axtgpasch  28698  axtgcont1  28699  tglng  28777  chdmm1i  31766  chm0i  31779  ledii  31825  lejdii  31827  pjoml2i  31874  pjoml4i  31876  cmcmlem  31880  cmbr4i  31890  osumcori  31932  pjssmii  31970  mayete3i  32017  riesz4  32353  riesz1  32354  cnlnadjeu  32367  nmopadjlei  32377  pjclem1  32484  pjci  32489  mdbr3  32586  mdbr4  32587  dmdbr2  32592  dmdbr5  32597  ssmd2  32601  mdslj1i  32608  mdslj2i  32609  mdsl1i  32610  mdsl2bi  32612  mdslmd1lem1  32614  mdslmd1lem2  32615  mdslmd2i  32619  csmdsymi  32623  cvexchlem  32657  atomli  32671  atcvat4i  32686  difininv  32800  disjxpin  32870  imadifxp  32883  off2  32923  mptiffisupp  32975  indsumin  33118  indf1ofs  33123  idlinsubrg  33679  ressply1invg  33800  evls1subd  33803  algextdeglem7  34054  algextdeglem8  34055  ordtrestNEW  34252  pnfneige0  34282  lmxrge0  34283  qqhnm  34321  qqhcn  34322  rrhre  34352  gsumesum  34390  esumlub  34391  esumcst  34394  esumpcvgval  34409  hasheuni  34416  esumcvg  34417  sigainb  34467  carsgclctunlem2  34650  sibfinima  34670  sibfof  34671  eulerpartlemelr  34688  eulerpartlemgh  34709  eulerpartlemgf  34710  eulerpartlemgs2  34711  eulerpartlemn  34712  probmeasb  34761  cndprob01  34766  hashreprin  34948  reprfi2  34951  breprexpnat  34962  hgt750lemd  34976  hgt750lema  34985  tgoldbachgtde  34988  tgoldbachgtda  34989  tgoldbachgt  34991  bnj1293  35145  connpconn  35622  iccllysconn  35637  cvmsss2  35661  cvmcov2  35662  cvmopnlem  35665  cvmliftmolem2  35669  cvmlift2lem12  35701  mvrsfpw  35893  elmsta  35935  msubvrs  35947  mclsind  35957  nepss  36105  dfon2lem4  36171  trer  36712  neiin  36728  neibastop1  36755  neibastop2lem  36756  topmeet  36760  filnetlem3  36776  weiunfr  36863  elttcirr  36927  bj-disj2r  37548  bj-restpw  37617  bj-restb  37619  bj-restuni2  37623  bj-ablsscmn  37805  topdifinffinlem  37876  opnmbllem0  38190  mblfinlem4  38194  mbfposadd  38201  heibor1lem  38343  heiborlem1  38345  heiborlem3  38347  heiborlem10  38354  opidonOLD  38386  disjimin  39385  lshpinN  39648  lcvexchlem1  39693  lcvexchlem5  39697  pmod1i  40507  pmodN  40509  osumcllem7N  40621  pexmidlem4N  40632  dochdmj1  42049  dochexmidlem4  42122  lcfrlem25  42226  mapd1o  42307  mapdin  42321  elrfi  43310  elrfirn  43311  fnwe2lem2  43663  aomclem2  43667  lsmfgcl  43686  lmhmfgima  43696  lmhmfgsplit  43698  lmhmlnmsplit  43699  hbt  43742  ofoafg  43966  trrelind  44276  iunrelexp0  44313  isotone2  44660  grumnudlem  44880  ismnushort  44896  onfrALTlem3  45138  onfrALTlem2  45140  onfrALTlem3VD  45480  onfrALTlem2VD  45482  iunconnlem2  45528  wfac8prim  45596  restuni6  45725  disjinfi  45795  inmap  45810  fsumiunss  46176  islptre  46220  sumnnodd  46231  limcresiooub  46241  limcresioolb  46242  limcleqr  46243  limclner  46250  limclr  46254  limsuplesup  46298  limsuppnfdlem  46300  limsupres  46304  liminfgord  46353  liminfgf  46357  liminfcl  46362  limsupresxr  46365  liminfresxr  46366  liminfval2  46367  liminflelimsuplem  46374  liminfvalxr  46382  icccncfext  46486  fourierdlem20  46726  fourierdlem48  46753  fourierdlem49  46754  fourierdlem50  46755  fourierdlem76  46781  fourierdlem103  46808  fourierdlem104  46809  fourierdlem113  46818  fouriersw  46830  salgencntex  46942  sge0less  46991  sge0resplit  47005  sge0split  47008  sge0iunmptlemre  47014  sge0fodjrnlem  47015  caragencmpl  47134  ovolval2lem  47242  ovolval2  47243  ovolval3  47246  ovolval4lem2  47249  sssmf  47337  nthrucw  47487  fcoreslem4  47685  fcoresf1  47688  fcoresfo  47690  3f1oss1  47694  rngchomrnghmresALTV  48926  termc  50175