Theorem inss2 4245

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 4216	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4244	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 4030	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  inindif  4380  difin0  4479  iunxdif3  5099  relin2  5825  relres  6025  idssxp  6068  ssrnres  6199  cnvrescnv  6216  ordin  6415  onfr  6424  ordelinel  6486  fnresin2  6694  fresaunres2  6780  ssimaex  6993  exfo  7124  ffvresb  7144  fnfvimad  7253  ofrfvalg  7704  ofval  7707  ofrval  7708  off  7714  ofres  7715  ofco  7721  fnwelem  8154  fnse  8156  fprlem1  8323  tfrlem5  8418  pmresg  8908  ixpfi2  9387  elfiun  9467  marypha1lem  9470  ordtypelem6  9560  ordtypelem7  9561  hartogslem1  9579  unxpwdom  9626  epfrs  9768  tcmin  9778  bnd2  9930  tskwe  9987  r0weon  10049  infxpenlem  10050  djuinf  10226  ackbij1lem9  10264  ackbij1lem10  10265  ackbij1lem15  10270  ackbij1lem16  10271  ackbij1b  10275  sdom2en01  10339  fin23lem26  10362  fin23lem13  10369  isfin1-3  10423  fin56  10430  fin1a2lem9  10445  brdom3  10565  brdom5  10566  brdom4  10567  fpwwe2lem11  10678  fpwwe2  10680  canthwelem  10687  gruima  10839  ingru  10852  gruina  10855  grur1a  10856  ltrelpi  10926  ltrelnq  10963  nqerf  10967  fzfi  14009  xptrrel  15015  rexanuz  15380  limsupgord  15504  limsupcl  15505  limsupgf  15507  limsupgle  15509  o1of2  15645  o1rlimmul  15651  ackbijnn  15860  bitsinv1  16475  bitsinvp1  16482  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  sadeq  16505  smupval  16521  prmrec  16955  structcnvcnv  17186  ressbasss  17283  ressbasssOLD  17284  ressress  17293  restsspw  17477  submre  17649  isacs1i  17701  rescabs  17882  rescabsOLD  17883  resscat  17902  funcres2c  17954  ressffth  17991  catccatid  18159  catcisolem  18163  catciso  18164  yoniso  18341  acsinfd  18613  acsdomd  18614  tsrss  18646  idresefmnd  18924  idrespermg  19443  mvdco  19477  lsmmod  19707  rnghmresfn  20635  rnghmsscmap  20646  rhmresfn  20664  rhmsscmap  20675  rhmsubclem4  20704  acsfn1p  20816  lssacs  20982  lidlssbas  21240  zringlpirlem2  21491  zringlpirlem3  21492  asplss  21911  ressmplbas  22063  subrgmpl  22067  mplind  22111  ressply1bas  22245  pf1rcl  22368  ressply1evl  22389  evls1addd  22390  evls1muld  22391  evls1vsca  22392  evls1maprhm  22395  ofco2  22472  basdif0  22975  eltg4i  22982  ntrss2  23080  ntrin  23084  isopn3  23089  resttopon  23184  restuni2  23190  restcld  23195  restfpw  23202  neitr  23203  cnrest2r  23310  cnpresti  23311  cnprest  23312  lmss  23321  cnrmi  23383  restcnrm  23385  resthauslem  23386  imacmp  23420  fiuncmp  23427  subislly  23504  islly2  23507  cldllycmp  23518  hauspwdom  23524  kgeni  23560  llycmpkgen2  23573  ptbasfi  23604  ptclsg  23638  ptcnplem  23644  txtube  23663  txcmplem2  23665  txkgen  23675  kqdisj  23755  fbasrn  23907  trfg  23914  isufil2  23931  fmfnfmlem4  23980  hauspwpwf1  24010  txflf  24029  alexsubALTlem4  24073  tmdgsum2  24119  tsmsres  24167  tsmsxplem1  24176  ustexsym  24239  ustund  24245  trust  24253  utoptop  24258  restutop  24261  metrest  24552  restmetu  24598  tgioo  24831  reconnlem2  24862  cphsqrtcl  25231  tcphcph  25284  cfilresi  25342  caussi  25344  causs  25345  ovolfioo  25515  ovolficc  25516  ovolficcss  25517  ovolfsf  25519  ovollb  25527  ovolicc2lem1  25565  ovolicc2lem2  25566  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2  25570  nulmbl  25583  voliunlem1  25598  ovolfs2  25619  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombllem6  25636  uniioombl  25637  dyadmbllem  25647  dyadmbl  25648  opnmbllem  25649  volcn  25654  volivth  25655  mbfadd  25709  mbfsub  25710  i1fima  25726  i1fima2  25727  i1fd  25729  i1fadd  25743  i1fmul  25744  itg1addlem2  25745  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  i1fres  25754  mbfmul  25775  bddmulibl  25888  ellimc2  25926  ellimc3  25928  limcflf  25930  limcresi  25934  limciun  25943  dvreslem  25958  dvres2lem  25959  dvres3a  25963  cpnres  25987  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvmptres3  26008  lhop1lem  26066  rlimcnp2  27023  xrlimcnp  27025  chpchtsum  27277  2sqlem8  27484  2sqlem9  27485  rpvmasumlem  27545  rplogsum  27585  dirith2  27586  nosupbnd2  27775  axtgsegcon  28486  axtg5seg  28487  axtgbtwnid  28488  axtgpasch  28489  axtgcont1  28490  tglng  28568  chdmm1i  31505  chm0i  31518  ledii  31564  lejdii  31566  pjoml2i  31613  pjoml4i  31615  cmcmlem  31619  cmbr4i  31629  osumcori  31671  pjssmii  31709  mayete3i  31756  riesz4  32092  riesz1  32093  cnlnadjeu  32106  nmopadjlei  32116  pjclem1  32223  pjci  32228  mdbr3  32325  mdbr4  32326  dmdbr2  32331  dmdbr5  32336  ssmd2  32340  mdslj1i  32347  mdslj2i  32348  mdsl1i  32349  mdsl2bi  32351  mdslmd1lem1  32353  mdslmd1lem2  32354  mdslmd2i  32358  csmdsymi  32362  cvexchlem  32396  atomli  32410  atcvat4i  32425  difininv  32544  disjxpin  32607  imadifxp  32620  off2  32657  mptiffisupp  32707  resspos  32940  resstos  32941  submomnd  33069  suborng  33324  idlinsubrg  33438  ressply1invg  33573  evls1subd  33576  algextdeglem7  33728  algextdeglem8  33729  ordtrestNEW  33881  pnfneige0  33911  lmxrge0  33912  qqhnm  33952  qqhcn  33953  rrhre  33983  indsumin  34002  indf1ofs  34006  gsumesum  34039  esumlub  34040  esumcst  34043  esumpcvgval  34058  hasheuni  34065  esumcvg  34066  sigainb  34116  carsgclctunlem2  34300  sibfinima  34320  sibfof  34321  eulerpartlemelr  34338  eulerpartlemgh  34359  eulerpartlemgf  34360  eulerpartlemgs2  34361  eulerpartlemn  34362  probmeasb  34411  cndprob01  34416  hashreprin  34613  reprfi2  34616  breprexpnat  34627  hgt750lemd  34641  hgt750lema  34650  tgoldbachgtde  34653  tgoldbachgtda  34654  tgoldbachgt  34656  bnj1293  34808  connpconn  35219  iccllysconn  35234  cvmsss2  35258  cvmcov2  35259  cvmopnlem  35262  cvmliftmolem2  35266  cvmlift2lem12  35298  mvrsfpw  35490  elmsta  35532  msubvrs  35544  mclsind  35554  nepss  35697  dfon2lem4  35767  trer  36298  neiin  36314  neibastop1  36341  neibastop2lem  36342  topmeet  36346  filnetlem3  36362  weiunfr  36449  bj-disj2r  37010  bj-restpw  37074  bj-restb  37076  bj-restuni2  37080  bj-ablsscmn  37260  topdifinffinlem  37329  opnmbllem0  37642  mblfinlem4  37646  mbfposadd  37653  heibor1lem  37795  heiborlem1  37797  heiborlem3  37799  heiborlem10  37806  opidonOLD  37838  disjimin  38732  lshpinN  38970  lcvexchlem1  39015  lcvexchlem5  39019  pmod1i  39830  pmodN  39832  osumcllem7N  39944  pexmidlem4N  39955  dochdmj1  41372  dochexmidlem4  41445  lcfrlem25  41549  mapd1o  41630  mapdin  41644  elrfi  42681  elrfirn  42682  fnwe2lem2  43039  aomclem2  43043  lsmfgcl  43062  lmhmfgima  43072  lmhmfgsplit  43074  lmhmlnmsplit  43075  hbt  43118  ofoafg  43343  trrelind  43654  iunrelexp0  43691  isotone2  44038  grumnudlem  44280  ismnushort  44296  onfrALTlem3  44541  onfrALTlem2  44543  onfrALTlem3VD  44884  onfrALTlem2VD  44886  iunconnlem2  44932  restuni6  45061  disjinfi  45134  inmap  45151  fsumiunss  45530  islptre  45574  sumnnodd  45585  limcresiooub  45597  limcresioolb  45598  limcleqr  45599  limclner  45606  limclr  45610  limsuplesup  45654  limsuppnfdlem  45656  limsupres  45660  liminfgord  45709  liminfgf  45713  liminfcl  45718  limsupresxr  45721  liminfresxr  45722  liminfval2  45723  liminflelimsuplem  45730  liminfvalxr  45738  icccncfext  45842  fourierdlem20  46082  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem76  46137  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  fouriersw  46186  salgencntex  46298  sge0less  46347  sge0resplit  46361  sge0split  46364  sge0iunmptlemre  46370  sge0fodjrnlem  46371  caragencmpl  46490  ovolval2lem  46598  ovolval2  46599  ovolval3  46602  ovolval4lem2  46605  sssmf  46693  fcoreslem4  47015  fcoresf1  47018  fcoresfo  47020  3f1oss1  47024  rngchomrnghmresALTV  48122