Theorem inss2 4137

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 4109	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4136	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3960	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

This proof depends on syntax axioms:   ⊆ wss 3900   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  inindif  4327  vvin  4362  difin0  4431  uniin  4896  iunxdif3  5060  relin2  5800  relresOLD  6013  idssxp  6059  rnin  6155  ssrnres  6188  cnvrescnv  6206  ordin  6419  onfr  6428  ordelinel  6492  fnresin2  6695  fresaunres2  6784  ssimaex  7001  exfo  7137  ffvresb  7158  fnfvimad  7271  ofrfvalg  7733  ofval  7736  ofrval  7737  off  7743  ofres  7744  ofco  7750  fnwelem  8180  fnwe2lem3  8184  fnse  8187  fprlem1  8356  tfrlem5  8425  pmresg  8936  ixpfi2  9377  elfiun  9459  marypha1lem  9462  ordtypelem6  9554  ordtypelem7  9555  hartogslem1  9573  unxpwdom  9620  epfrs  9769  tcmin  9777  bnd2  9993  tskwe  10068  r0weon  10130  infxpenlem  10131  djuinf  10306  ackbij1lem9  10344  ackbij1lem10  10345  ackbij1lem15  10350  ackbij1lem16  10351  ackbij1b  10355  sdom2en01  10419  fin23lem26  10442  fin23lem13  10449  isfin1-3  10503  fin56  10510  fin1a2lem9  10525  brdom3  10646  brdom5  10647  brdom4  10648  fpwwe2lem11  10765  fpwwe2  10767  canthwelem  10774  gruima  10926  ingru  10939  gruina  10942  grur1a  10943  ltrelpi  11013  ltrelnq  11050  nqerf  11054  fzfi  14155  xptrrel  15176  rexanuz  15557  limsupgord  15683  limsupcl  15684  limsupgf  15686  limsupgle  15688  o1of2  15824  o1rlimmul  15830  ackbijnn  16041  bitsinv1  16656  bitsinvp1  16663  sadcaddlem  16671  sadadd2lem  16673  sadadd3  16675  sadaddlem  16680  sadasslem  16684  sadeq  16686  smupval  16702  prmrec  17144  structcnvcnv  17375  ressbasss  17461  ressbasssOLD  17462  ressress  17469  restsspw  17652  submre  17825  isacs1i  17881  rescabs  18058  resscat  18077  funcres2c  18128  ressffth  18165  catccatid  18331  catcisolem  18335  catciso  18336  yoniso  18509  resspos  18653  resstos  18654  acsinfd  18780  acsdomd  18781  tsrss  18813  idresefmnd  19145  idrespermg  19676  mvdco  19710  lsmmod  19940  submomnd  20397  rnghmresfn  20922  rnghmsscmap  20933  rhmresfn  20951  rhmsscmap  20962  rhmsubclem4  20991  acsfn1p  21107  suborng  21184  lssacs  21293  lidlssbas  21543  zringlpirlem2  21824  zringlpirlem3  21825  asplss  22236  ressmplbas  22391  subrgmpl  22395  mplind  22434  ressply1bas  22601  pf1rcl  22722  ressply1evl  22743  evls1addd  22744  evls1muld  22745  evls1vsca  22746  evls1maprhm  22749  ofco2  22821  basdif0  23326  eltg4i  23333  ntrss2  23430  ntrin  23434  isopn3  23439  resttopon  23534  restuni2  23540  restcld  23545  restfpw  23552  neitr  23553  cnrest2r  23660  cnpresti  23661  cnprest  23662  lmss  23671  cnrmi  23733  restcnrm  23735  resthauslem  23736  imacmp  23770  fiuncmp  23777  subislly  23855  islly2  23858  cldllycmp  23869  hauspwdom  23875  kgeni  23911  llycmpkgen2  23924  ptbasfi  23955  ptclsg  23989  ptcnplem  23995  txtube  24014  txcmplem2  24016  txkgen  24026  kqdisj  24106  fbasrn  24258  trfg  24265  isufil2  24282  fmfnfmlem4  24331  hauspwpwf1  24361  txflf  24380  alexsubALTlem4  24424  tmdgsum2  24470  tsmsres  24518  tsmsxplem1  24527  ustexsym  24590  ustund  24596  trust  24603  utoptop  24608  restutop  24611  metrest  24898  restmetu  24944  tgioo  25170  reconnlem2  25202  cphsqrtcl  25560  tcphcph  25613  cfilresi  25671  caussi  25673  causs  25674  ovolfioo  25843  ovolficc  25844  ovolficcss  25845  ovolfsf  25847  ovollb  25855  ovolicc2lem1  25893  ovolicc2lem2  25894  ovolicc2lem3  25895  ovolicc2lem4  25896  ovolicc2  25898  nulmbl  25911  voliunlem1  25926  ovolfs2  25947  uniiccdif  25954  uniioovol  25955  uniiccvol  25956  uniioombllem2  25959  uniioombllem3a  25960  uniioombllem3  25961  uniioombllem4  25962  uniioombllem5  25963  uniioombllem6  25964  uniioombl  25965  dyadmbllem  25975  dyadmbl  25976  opnmbllem  25977  volcn  25982  volivth  25983  mbfadd  26037  mbfsub  26038  i1fima  26054  i1fima2  26055  i1fd  26057  i1fadd  26071  i1fmul  26072  itg1addlem2  26073  itg1addlem4  26075  itg1addlem5  26076  i1fres  26081  mbfmul  26102  bddmulibl  26214  ellimc2  26252  ellimc3  26254  limcflf  26256  limcresi  26260  limciun  26269  dvreslem  26284  dvres2lem  26285  dvres3a  26289  cpnres  26312  dvaddbr  26313  dvmulbr  26314  dvmptres3  26331  lhop1lem  26388  rlimcnp2  27351  xrlimcnp  27353  chpchtsum  27603  2sqlem8  27810  2sqlem9  27811  rpvmasumlem  27871  rplogsum  27911  dirith2  27912  nosupbnd2  28130  axtgsegcon  28983  axtg5seg  28984  axtgbtwnid  28985  axtgpasch  28986  axtgcont1  28987  tglng  29066  chdmm1i  32136  chm0i  32149  ledii  32195  lejdii  32197  pjoml2i  32244  pjoml4i  32246  cmcmlem  32250  cmbr4i  32260  osumcori  32302  pjssmii  32340  mayete3i  32387  riesz4  32723  riesz1  32724  cnlnadjeu  32737  nmopadjlei  32747  pjclem1  32854  pjci  32859  mdbr3  32956  mdbr4  32957  dmdbr2  32962  dmdbr5  32967  ssmd2  32971  mdslj1i  32978  mdslj2i  32979  mdsl1i  32980  mdsl2bi  32982  mdslmd1lem1  32984  mdslmd1lem2  32985  mdslmd2i  32989  csmdsymi  32993  cvexchlem  33027  atomli  33041  atcvat4i  33056  difininv  33212  disjxpin  33280  imadifxp  33293  off2  33333  mptiffisupp  33383  indsumin  33524  indf1ofs  33529  idlinsubrg  34085  ressply1invg  34204  evls1subd  34207  algextdeglem7  34466  algextdeglem8  34467  ordtrestNEW  34664  pnfneige0  34694  lmxrge0  34695  qqhnm  34733  qqhcn  34734  rrhre  34764  gsumesum  34802  esumlub  34803  esumcst  34806  esumpcvgval  34821  hasheuni  34828  esumcvg  34829  sigainb  34880  carsgclctunlem2  35062  sibfinima  35082  sibfof  35083  eulerpartlemelr  35100  eulerpartlemgh  35121  eulerpartlemgf  35122  eulerpartlemgs2  35123  eulerpartlemn  35124  probmeasb  35173  cndprob01  35178  hashreprin  35360  reprfi2  35363  breprexpnat  35374  hgt750lemd  35388  hgt750lema  35397  tgoldbachgtde  35400  tgoldbachgtda  35401  tgoldbachgt  35403  bnj1293  35557  weexenwe  35889  connpconn  36208  iccllysconn  36223  cvmsss2  36247  cvmcov2  36248  cvmopnlem  36251  cvmliftmolem2  36255  cvmlift2lem12  36287  mvrsfpw  36479  elmsta  36521  msubvrs  36533  mclsind  36543  nepss  36698  dfon2lem4  36763  trer  37319  neiin  37335  neibastop1  37362  neibastop2lem  37363  topmeet  37367  filnetlem3  37383  weiunfr  37470  elttcirr  37534  bj-disj2r  38156  resss2  38180  coindiss  38205  coindirss  38206  nvo3  38230  bj-restpw  38283  bj-restb  38285  bj-restuni2  38289  bj-ablsscmn  38467  topdifinffinlem  38538  opnmbllem0  38842  mblfinlem4  38846  mbfposadd  38853  heibor1lem  39009  heiborlem1  39011  heiborlem3  39013  heiborlem10  39020  opidonOLD  39052  disjimin  40049  lshpinN  40312  lcvexchlem1  40357  lcvexchlem5  40361  pmod1i  41171  pmodN  41173  osumcllem7N  41285  pexmidlem4N  41296  dochdmj1  42713  dochexmidlem4  42786  lcfrlem25  42890  mapd1o  42971  mapdin  42985  elrfi  43971  elrfirn  43972  aomclem2  44323  lsmfgcl  44342  lmhmfgima  44352  lmhmfgsplit  44354  lmhmlnmsplit  44355  hbt  44397  ofoafg  44617  trrelind  44926  iunrelexp0  44963  isotone2  45310  grumnudlem  45530  ismnushort  45546  onfrALTlem3  45787  onfrALTlem2  45789  onfrALTlem3VD  46129  onfrALTlem2VD  46131  iunconnlem2  46177  wfac8prim  46256  restuni6  46410  disjinfi  46480  inmap  46495  fsumiunss  46860  islptre  46904  sumnnodd  46915  limcresiooub  46925  limcresioolb  46926  limcleqr  46927  limclner  46934  limclr  46938  limsuplesup  46982  limsuppnfdlem  46984  limsupres  46988  liminfgord  47037  liminfgf  47041  liminfcl  47046  limsupresxr  47049  liminfresxr  47050  liminfval2  47051  liminflelimsuplem  47058  liminfvalxr  47066  icccncfext  47170  fourierdlem20  47410  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem76  47465  fourierdlem103  47492  fourierdlem104  47493  fourierdlem113  47502  fouriersw  47514  salgencntex  47626  sge0less  47675  sge0resplit  47689  sge0split  47692  sge0iunmptlemre  47698  sge0fodjrnlem  47699  caragencmpl  47818  ovolval2lem  47926  ovolval2  47927  ovolval3  47930  ovolval4lem2  47933  sssmf  48021  wrddrin  48170  chndrin  48175  chnrrin  48180  numtowerdt  48189  tmachlem-fssscan  48233  fcoreslem4  48409  fcoresf1  48412  fcoresfo  48414  3f1oss1  48418  rngchomrnghmresALTV  49649  termc  50985