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 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 3420  df-v 3465  df-in 3938  df-ss 3948

This theorem is referenced by:  inindif  4355  difin0  4454  iunxdif3  5075  relin2  5803  relres  6003  idssxp  6047  ssrnres  6178  cnvrescnv  6195  ordin  6393  onfr  6402  ordelinel  6465  fnresin2  6674  fresaunres2  6760  ssimaex  6974  exfo  7105  ffvresb  7125  fnfvimad  7236  ofrfvalg  7687  ofval  7690  ofrval  7691  off  7697  ofres  7698  ofco  7704  fnwelem  8138  fnse  8140  fprlem1  8307  tfrlem5  8402  pmresg  8892  ixpfi2  9372  elfiun  9452  marypha1lem  9455  ordtypelem6  9545  ordtypelem7  9546  hartogslem1  9564  unxpwdom  9611  epfrs  9753  tcmin  9763  bnd2  9915  tskwe  9972  r0weon  10034  infxpenlem  10035  djuinf  10211  ackbij1lem9  10249  ackbij1lem10  10250  ackbij1lem15  10255  ackbij1lem16  10256  ackbij1b  10260  sdom2en01  10324  fin23lem26  10347  fin23lem13  10354  isfin1-3  10408  fin56  10415  fin1a2lem9  10430  brdom3  10550  brdom5  10551  brdom4  10552  fpwwe2lem11  10663  fpwwe2  10665  canthwelem  10672  gruima  10824  ingru  10837  gruina  10840  grur1a  10841  ltrelpi  10911  ltrelnq  10948  nqerf  10952  fzfi  13995  xptrrel  15001  rexanuz  15366  limsupgord  15490  limsupcl  15491  limsupgf  15493  limsupgle  15495  o1of2  15631  o1rlimmul  15637  ackbijnn  15846  bitsinv1  16461  bitsinvp1  16468  sadcaddlem  16476  sadadd2lem  16478  sadadd3  16480  sadaddlem  16485  sadasslem  16489  sadeq  16491  smupval  16507  prmrec  16942  structcnvcnv  17172  ressbasss  17262  ressbasssOLD  17263  ressress  17270  restsspw  17447  submre  17619  isacs1i  17671  rescabs  17848  rescabsOLD  17849  resscat  17868  funcres2c  17919  ressffth  17956  catccatid  18122  catcisolem  18126  catciso  18127  yoniso  18300  acsinfd  18570  acsdomd  18571  tsrss  18603  idresefmnd  18881  idrespermg  19397  mvdco  19431  lsmmod  19661  rnghmresfn  20587  rnghmsscmap  20598  rhmresfn  20616  rhmsscmap  20627  rhmsubclem4  20656  acsfn1p  20768  lssacs  20933  lidlssbas  21185  zringlpirlem2  21436  zringlpirlem3  21437  asplss  21848  ressmplbas  22000  subrgmpl  22004  mplind  22042  ressply1bas  22178  pf1rcl  22301  ressply1evl  22322  evls1addd  22323  evls1muld  22324  evls1vsca  22325  evls1maprhm  22328  ofco2  22405  basdif0  22907  eltg4i  22914  ntrss2  23011  ntrin  23015  isopn3  23020  resttopon  23115  restuni2  23121  restcld  23126  restfpw  23133  neitr  23134  cnrest2r  23241  cnpresti  23242  cnprest  23243  lmss  23252  cnrmi  23314  restcnrm  23316  resthauslem  23317  imacmp  23351  fiuncmp  23358  subislly  23435  islly2  23438  cldllycmp  23449  hauspwdom  23455  kgeni  23491  llycmpkgen2  23504  ptbasfi  23535  ptclsg  23569  ptcnplem  23575  txtube  23594  txcmplem2  23596  txkgen  23606  kqdisj  23686  fbasrn  23838  trfg  23845  isufil2  23862  fmfnfmlem4  23911  hauspwpwf1  23941  txflf  23960  alexsubALTlem4  24004  tmdgsum2  24050  tsmsres  24098  tsmsxplem1  24107  ustexsym  24170  ustund  24176  trust  24184  utoptop  24189  restutop  24192  metrest  24481  restmetu  24527  tgioo  24753  reconnlem2  24785  cphsqrtcl  25154  tcphcph  25207  cfilresi  25265  caussi  25267  causs  25268  ovolfioo  25438  ovolficc  25439  ovolficcss  25440  ovolfsf  25442  ovollb  25450  ovolicc2lem1  25488  ovolicc2lem2  25489  ovolicc2lem3  25490  ovolicc2lem4  25491  ovolicc2  25493  nulmbl  25506  voliunlem1  25521  ovolfs2  25542  uniiccdif  25549  uniioovol  25550  uniiccvol  25551  uniioombllem2  25554  uniioombllem3a  25555  uniioombllem3  25556  uniioombllem4  25557  uniioombllem5  25558  uniioombllem6  25559  uniioombl  25560  dyadmbllem  25570  dyadmbl  25571  opnmbllem  25572  volcn  25577  volivth  25578  mbfadd  25632  mbfsub  25633  i1fima  25649  i1fima2  25650  i1fd  25652  i1fadd  25666  i1fmul  25667  itg1addlem2  25668  itg1addlem4  25670  itg1addlem5  25671  i1fres  25676  mbfmul  25697  bddmulibl  25810  ellimc2  25848  ellimc3  25850  limcflf  25852  limcresi  25856  limciun  25865  dvreslem  25880  dvres2lem  25881  dvres3a  25885  cpnres  25909  dvaddbr  25910  dvmulbr  25911  dvmulbrOLD  25912  dvmptres3  25930  lhop1lem  25988  rlimcnp2  26945  xrlimcnp  26947  chpchtsum  27199  2sqlem8  27406  2sqlem9  27407  rpvmasumlem  27467  rplogsum  27507  dirith2  27508  nosupbnd2  27697  axtgsegcon  28408  axtg5seg  28409  axtgbtwnid  28410  axtgpasch  28411  axtgcont1  28412  tglng  28490  chdmm1i  31424  chm0i  31437  ledii  31483  lejdii  31485  pjoml2i  31532  pjoml4i  31534  cmcmlem  31538  cmbr4i  31548  osumcori  31590  pjssmii  31628  mayete3i  31675  riesz4  32011  riesz1  32012  cnlnadjeu  32025  nmopadjlei  32035  pjclem1  32142  pjci  32147  mdbr3  32244  mdbr4  32245  dmdbr2  32250  dmdbr5  32255  ssmd2  32259  mdslj1i  32266  mdslj2i  32267  mdsl1i  32268  mdsl2bi  32270  mdslmd1lem1  32272  mdslmd1lem2  32273  mdslmd2i  32277  csmdsymi  32281  cvexchlem  32315  atomli  32329  atcvat4i  32344  difininv  32464  disjxpin  32536  imadifxp  32549  off2  32586  mptiffisupp  32637  indsumin  32787  indf1ofs  32791  resspos  32895  resstos  32896  submomnd  33026  suborng  33285  idlinsubrg  33394  ressply1invg  33529  evls1subd  33532  algextdeglem7  33703  algextdeglem8  33704  ordtrestNEW  33879  pnfneige0  33909  lmxrge0  33910  qqhnm  33950  qqhcn  33951  rrhre  33981  gsumesum  34019  esumlub  34020  esumcst  34023  esumpcvgval  34038  hasheuni  34045  esumcvg  34046  sigainb  34096  carsgclctunlem2  34280  sibfinima  34300  sibfof  34301  eulerpartlemelr  34318  eulerpartlemgh  34339  eulerpartlemgf  34340  eulerpartlemgs2  34341  eulerpartlemn  34342  probmeasb  34391  cndprob01  34396  hashreprin  34594  reprfi2  34597  breprexpnat  34608  hgt750lemd  34622  hgt750lema  34631  tgoldbachgtde  34634  tgoldbachgtda  34635  tgoldbachgt  34637  bnj1293  34789  connpconn  35199  iccllysconn  35214  cvmsss2  35238  cvmcov2  35239  cvmopnlem  35242  cvmliftmolem2  35246  cvmlift2lem12  35278  mvrsfpw  35470  elmsta  35512  msubvrs  35524  mclsind  35534  nepss  35677  dfon2lem4  35746  trer  36276  neiin  36292  neibastop1  36319  neibastop2lem  36320  topmeet  36324  filnetlem3  36340  weiunfr  36427  bj-disj2r  36988  bj-restpw  37052  bj-restb  37054  bj-restuni2  37058  bj-ablsscmn  37238  topdifinffinlem  37307  opnmbllem0  37622  mblfinlem4  37626  mbfposadd  37633  heibor1lem  37775  heiborlem1  37777  heiborlem3  37779  heiborlem10  37786  opidonOLD  37818  disjimin  38711  lshpinN  38949  lcvexchlem1  38994  lcvexchlem5  38998  pmod1i  39809  pmodN  39811  osumcllem7N  39923  pexmidlem4N  39934  dochdmj1  41351  dochexmidlem4  41424  lcfrlem25  41528  mapd1o  41609  mapdin  41623  elrfi  42668  elrfirn  42669  fnwe2lem2  43026  aomclem2  43030  lsmfgcl  43049  lmhmfgima  43059  lmhmfgsplit  43061  lmhmlnmsplit  43062  hbt  43105  ofoafg  43329  trrelind  43640  iunrelexp0  43677  isotone2  44024  grumnudlem  44261  ismnushort  44277  onfrALTlem3  44521  onfrALTlem2  44523  onfrALTlem3VD  44864  onfrALTlem2VD  44866  iunconnlem2  44912  wfac8prim  44976  restuni6  45084  disjinfi  45154  inmap  45171  fsumiunss  45547  islptre  45591  sumnnodd  45602  limcresiooub  45614  limcresioolb  45615  limcleqr  45616  limclner  45623  limclr  45627  limsuplesup  45671  limsuppnfdlem  45673  limsupres  45677  liminfgord  45726  liminfgf  45730  liminfcl  45735  limsupresxr  45738  liminfresxr  45739  liminfval2  45740  liminflelimsuplem  45747  liminfvalxr  45755  icccncfext  45859  fourierdlem20  46099  fourierdlem48  46126  fourierdlem49  46127  fourierdlem50  46128  fourierdlem76  46154  fourierdlem103  46181  fourierdlem104  46182  fourierdlem113  46191  fouriersw  46203  salgencntex  46315  sge0less  46364  sge0resplit  46378  sge0split  46381  sge0iunmptlemre  46387  sge0fodjrnlem  46388  caragencmpl  46507  ovolval2lem  46615  ovolval2  46616  ovolval3  46619  ovolval4lem2  46622  sssmf  46710  fcoreslem4  47036  fcoresf1  47039  fcoresfo  47041  3f1oss1  47045  rngchomrnghmresALTV  48153  termc  49130