Theorem inss2 4225

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

Syntax hints:   ∩ cin 3943   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  difin0  4469  iunxdif3  5092  relin2  5809  relres  6008  idssxp  6046  ssrnres  6176  cnvrescnv  6193  ordin  6393  onfr  6402  ordelinel  6464  fnresin2  6675  fresaunres2  6763  ssimaex  6977  exfo  7109  ffvresb  7129  fnfvimad  7240  ofrfvalg  7687  ofval  7690  ofrval  7691  off  7697  ofres  7698  ofco  7702  fnwelem  8130  fnse  8132  fprlem1  8299  tfrlem5  8394  pmresg  8880  nnfiOLD  9248  ixpfi2  9366  elfiun  9445  marypha1lem  9448  ordtypelem6  9538  ordtypelem7  9539  hartogslem1  9557  unxpwdom  9604  epfrs  9746  tcmin  9756  bnd2  9908  tskwe  9965  r0weon  10027  infxpenlem  10028  djuinf  10203  ackbij1lem9  10243  ackbij1lem10  10244  ackbij1lem15  10249  ackbij1lem16  10250  ackbij1b  10254  sdom2en01  10317  fin23lem26  10340  fin23lem13  10347  isfin1-3  10401  fin56  10408  fin1a2lem9  10423  brdom3  10543  brdom5  10544  brdom4  10545  fpwwe2lem11  10656  fpwwe2  10658  canthwelem  10665  gruima  10817  ingru  10830  gruina  10833  grur1a  10834  ltrelpi  10904  ltrelnq  10941  nqerf  10945  fzfi  13961  xptrrel  14951  rexanuz  15316  limsupgord  15440  limsupcl  15441  limsupgf  15443  limsupgle  15445  o1of2  15581  o1rlimmul  15587  ackbijnn  15798  bitsinv1  16408  bitsinvp1  16415  sadcaddlem  16423  sadadd2lem  16425  sadadd3  16427  sadaddlem  16432  sadasslem  16436  sadeq  16438  smupval  16454  prmrec  16882  structcnvcnv  17113  ressbasss  17210  ressbasssOLD  17211  ressress  17220  restsspw  17404  submre  17576  isacs1i  17628  rescabs  17809  rescabsOLD  17810  resscat  17829  funcres2c  17881  ressffth  17918  catccatid  18086  catcisolem  18090  catciso  18091  yoniso  18268  acsinfd  18539  acsdomd  18540  tsrss  18572  idresefmnd  18842  idrespermg  19357  mvdco  19391  lsmmod  19621  rnghmresfn  20541  rnghmsscmap  20552  rhmresfn  20570  rhmsscmap  20581  rhmsubclem4  20610  acsfn1p  20676  lssacs  20840  lidlssbas  21098  zringlpirlem2  21376  zringlpirlem3  21377  asplss  21794  ressmplbas  21953  subrgmpl  21957  mplind  22001  ressply1bas  22134  pf1rcl  22255  ofco2  22340  basdif0  22843  eltg4i  22850  ntrss2  22948  ntrin  22952  isopn3  22957  resttopon  23052  restuni2  23058  restcld  23063  restfpw  23070  neitr  23071  cnrest2r  23178  cnpresti  23179  cnprest  23180  lmss  23189  cnrmi  23251  restcnrm  23253  resthauslem  23254  imacmp  23288  fiuncmp  23295  subislly  23372  islly2  23375  cldllycmp  23386  hauspwdom  23392  kgeni  23428  llycmpkgen2  23441  ptbasfi  23472  ptclsg  23506  ptcnplem  23512  txtube  23531  txcmplem2  23533  txkgen  23543  kqdisj  23623  fbasrn  23775  trfg  23782  isufil2  23799  fmfnfmlem4  23848  hauspwpwf1  23878  txflf  23897  alexsubALTlem4  23941  tmdgsum2  23987  tsmsres  24035  tsmsxplem1  24044  ustexsym  24107  ustund  24113  trust  24121  utoptop  24126  restutop  24129  metrest  24420  restmetu  24466  tgioo  24699  reconnlem2  24730  cphsqrtcl  25099  tcphcph  25152  cfilresi  25210  caussi  25212  causs  25213  ovolfioo  25383  ovolficc  25384  ovolficcss  25385  ovolfsf  25387  ovollb  25395  ovolicc2lem1  25433  ovolicc2lem2  25434  ovolicc2lem3  25435  ovolicc2lem4  25436  ovolicc2  25438  nulmbl  25451  voliunlem1  25466  ovolfs2  25487  uniiccdif  25494  uniioovol  25495  uniiccvol  25496  uniioombllem2  25499  uniioombllem3a  25500  uniioombllem3  25501  uniioombllem4  25502  uniioombllem5  25503  uniioombllem6  25504  uniioombl  25505  dyadmbllem  25515  dyadmbl  25516  opnmbllem  25517  volcn  25522  volivth  25523  mbfadd  25577  mbfsub  25578  i1fima  25594  i1fima2  25595  i1fd  25597  i1fadd  25611  i1fmul  25612  itg1addlem2  25613  itg1addlem4  25615  itg1addlem4OLD  25616  itg1addlem5  25617  i1fres  25622  mbfmul  25643  bddmulibl  25755  ellimc2  25793  ellimc3  25795  limcflf  25797  limcresi  25801  limciun  25810  dvreslem  25825  dvres2lem  25826  dvres3a  25830  cpnres  25854  dvaddbr  25855  dvmulbr  25856  dvmulbrOLD  25857  dvmptres3  25875  lhop1lem  25933  rlimcnp2  26885  xrlimcnp  26887  chpchtsum  27139  2sqlem8  27346  2sqlem9  27347  rpvmasumlem  27407  rplogsum  27447  dirith2  27448  nosupbnd2  27636  axtgsegcon  28255  axtg5seg  28256  axtgbtwnid  28257  axtgpasch  28258  axtgcont1  28259  tglng  28337  chdmm1i  31274  chm0i  31287  ledii  31333  lejdii  31335  pjoml2i  31382  pjoml4i  31384  cmcmlem  31388  cmbr4i  31398  osumcori  31440  pjssmii  31478  mayete3i  31525  riesz4  31861  riesz1  31862  cnlnadjeu  31875  nmopadjlei  31885  pjclem1  31992  pjci  31997  mdbr3  32094  mdbr4  32095  dmdbr2  32100  dmdbr5  32105  ssmd2  32109  mdslj1i  32116  mdslj2i  32117  mdsl1i  32118  mdsl2bi  32120  mdslmd1lem1  32122  mdslmd1lem2  32123  mdslmd2i  32127  csmdsymi  32131  cvexchlem  32165  atomli  32179  atcvat4i  32194  inindif  32298  difininv  32299  disjxpin  32363  imadifxp  32376  off2  32410  mptiffisupp  32457  resspos  32675  resstos  32676  submomnd  32768  suborng  32970  idlinsubrg  33082  ressply1invg  33180  ressply1evl  33183  evls1addd  33184  evls1subd  33185  evls1muld  33186  evls1vsca  33187  evls1maprhm  33305  algextdeglem7  33327  algextdeglem8  33328  ordtrestNEW  33458  pnfneige0  33488  lmxrge0  33489  qqhnm  33527  qqhcn  33528  rrhre  33558  indsumin  33577  indf1ofs  33581  gsumesum  33614  esumlub  33615  esumcst  33618  esumpcvgval  33633  hasheuni  33640  esumcvg  33641  sigainb  33691  carsgclctunlem2  33875  sibfinima  33895  sibfof  33896  eulerpartlemelr  33913  eulerpartlemgh  33934  eulerpartlemgf  33935  eulerpartlemgs2  33936  eulerpartlemn  33937  probmeasb  33986  cndprob01  33991  hashreprin  34188  reprfi2  34191  breprexpnat  34202  hgt750lemd  34216  hgt750lema  34225  tgoldbachgtde  34228  tgoldbachgtda  34229  tgoldbachgt  34231  bnj1293  34383  connpconn  34781  iccllysconn  34796  cvmsss2  34820  cvmcov2  34821  cvmopnlem  34824  cvmliftmolem2  34828  cvmlift2lem12  34860  mvrsfpw  35052  elmsta  35094  msubvrs  35106  mclsind  35116  nepss  35248  dfon2lem4  35318  trer  35736  neiin  35752  neibastop1  35779  neibastop2lem  35780  topmeet  35784  filnetlem3  35800  bj-disj2r  36443  bj-restpw  36507  bj-restb  36509  bj-restuni2  36513  bj-ablsscmn  36693  topdifinffinlem  36762  opnmbllem0  37064  mblfinlem4  37068  mbfposadd  37075  heibor1lem  37217  heiborlem1  37219  heiborlem3  37221  heiborlem10  37228  opidonOLD  37260  disjimin  38160  lshpinN  38398  lcvexchlem1  38443  lcvexchlem5  38447  pmod1i  39258  pmodN  39260  osumcllem7N  39372  pexmidlem4N  39383  dochdmj1  40800  dochexmidlem4  40873  lcfrlem25  40977  mapd1o  41058  mapdin  41072  elrfi  42036  elrfirn  42037  fnwe2lem2  42397  aomclem2  42401  lsmfgcl  42420  lmhmfgima  42430  lmhmfgsplit  42432  lmhmlnmsplit  42433  hbt  42476  ofoafg  42706  trrelind  43018  iunrelexp0  43055  isotone2  43402  grumnudlem  43645  ismnushort  43661  onfrALTlem3  43906  onfrALTlem2  43908  onfrALTlem3VD  44249  onfrALTlem2VD  44251  iunconnlem2  44297  restuni6  44411  disjinfi  44488  inmap  44505  dmresss  44528  fsumiunss  44886  islptre  44930  sumnnodd  44941  limcresiooub  44953  limcresioolb  44954  limcleqr  44955  limclner  44962  limclr  44966  limsuplesup  45010  limsuppnfdlem  45012  limsupres  45016  liminfgord  45065  liminfgf  45069  liminfcl  45074  limsupresxr  45077  liminfresxr  45078  liminfval2  45079  liminflelimsuplem  45086  liminfvalxr  45094  icccncfext  45198  fourierdlem20  45438  fourierdlem48  45465  fourierdlem49  45466  fourierdlem50  45467  fourierdlem76  45493  fourierdlem103  45520  fourierdlem104  45521  fourierdlem113  45530  fouriersw  45542  salgencntex  45654  sge0less  45703  sge0resplit  45717  sge0split  45720  sge0iunmptlemre  45726  sge0fodjrnlem  45727  caragencmpl  45846  ovolval2lem  45954  ovolval2  45955  ovolval3  45958  ovolval4lem2  45961  sssmf  46049  fcoreslem4  46371  fcoresf1  46374  fcoresfo  46376  rngchomrnghmresALTV  47264