Theorem inss2 4229

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 4201	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4228	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 4017	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3947   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  difin0  4473  iunxdif3  5098  relin2  5812  relres  6009  idssxp  6047  ssrnres  6175  cnvrescnv  6192  ordin  6392  onfr  6401  ordelinel  6463  fnresin2  6674  fresaunres2  6761  ssimaex  6974  exfo  7104  ffvresb  7121  fnfvimad  7233  ofrfvalg  7675  ofval  7678  ofrval  7679  off  7685  ofres  7686  ofco  7690  fnwelem  8114  fnse  8116  fprlem1  8282  tfrlem5  8377  pmresg  8861  nnfiOLD  9229  ixpfi2  9347  elfiun  9422  marypha1lem  9425  ordtypelem6  9515  ordtypelem7  9516  hartogslem1  9534  unxpwdom  9581  epfrs  9723  tcmin  9733  bnd2  9885  tskwe  9942  r0weon  10004  infxpenlem  10005  djuinf  10180  ackbij1lem9  10220  ackbij1lem10  10221  ackbij1lem15  10226  ackbij1lem16  10227  ackbij1b  10231  sdom2en01  10294  fin23lem26  10317  fin23lem13  10324  isfin1-3  10378  fin56  10385  fin1a2lem9  10400  brdom3  10520  brdom5  10521  brdom4  10522  fpwwe2lem11  10633  fpwwe2  10635  canthwelem  10642  gruima  10794  ingru  10807  gruina  10810  grur1a  10811  ltrelpi  10881  ltrelnq  10918  nqerf  10922  fzfi  13934  xptrrel  14924  rexanuz  15289  limsupgord  15413  limsupcl  15414  limsupgf  15416  limsupgle  15418  o1of2  15554  o1rlimmul  15560  ackbijnn  15771  bitsinv1  16380  bitsinvp1  16387  sadcaddlem  16395  sadadd2lem  16397  sadadd3  16399  sadaddlem  16404  sadasslem  16408  sadeq  16410  smupval  16426  prmrec  16852  structcnvcnv  17083  ressbasss  17180  ressbasssOLD  17181  ressress  17190  restsspw  17374  submre  17546  isacs1i  17598  rescabs  17779  rescabsOLD  17780  resscat  17799  funcres2c  17849  ressffth  17886  catccatid  18053  catcisolem  18057  catciso  18058  yoniso  18235  acsinfd  18506  acsdomd  18507  tsrss  18539  idresefmnd  18777  idrespermg  19274  mvdco  19308  lsmmod  19538  acsfn1p  20408  lssacs  20571  zringlpirlem2  21025  zringlpirlem3  21026  asplss  21420  ressmplbas  21575  subrgmpl  21579  mplind  21623  ressply1bas  21743  pf1rcl  21860  ofco2  21945  basdif0  22448  eltg4i  22455  ntrss2  22553  ntrin  22557  isopn3  22562  resttopon  22657  restuni2  22663  restcld  22668  restfpw  22675  neitr  22676  cnrest2r  22783  cnpresti  22784  cnprest  22785  lmss  22794  cnrmi  22856  restcnrm  22858  resthauslem  22859  imacmp  22893  fiuncmp  22900  subislly  22977  islly2  22980  cldllycmp  22991  hauspwdom  22997  kgeni  23033  llycmpkgen2  23046  ptbasfi  23077  ptclsg  23111  ptcnplem  23117  txtube  23136  txcmplem2  23138  txkgen  23148  kqdisj  23228  fbasrn  23380  trfg  23387  isufil2  23404  fmfnfmlem4  23453  hauspwpwf1  23483  txflf  23502  alexsubALTlem4  23546  tmdgsum2  23592  tsmsres  23640  tsmsxplem1  23649  ustexsym  23712  ustund  23718  trust  23726  utoptop  23731  restutop  23734  metrest  24025  restmetu  24071  tgioo  24304  reconnlem2  24335  cphsqrtcl  24693  tcphcph  24746  cfilresi  24804  caussi  24806  causs  24807  ovolfioo  24976  ovolficc  24977  ovolficcss  24978  ovolfsf  24980  ovollb  24988  ovolicc2lem1  25026  ovolicc2lem2  25027  ovolicc2lem3  25028  ovolicc2lem4  25029  ovolicc2  25031  nulmbl  25044  voliunlem1  25059  ovolfs2  25080  uniiccdif  25087  uniioovol  25088  uniiccvol  25089  uniioombllem2  25092  uniioombllem3a  25093  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  uniioombllem6  25097  uniioombl  25098  dyadmbllem  25108  dyadmbl  25109  opnmbllem  25110  volcn  25115  volivth  25116  mbfadd  25170  mbfsub  25171  i1fima  25187  i1fima2  25188  i1fd  25190  i1fadd  25204  i1fmul  25205  itg1addlem2  25206  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  i1fres  25215  mbfmul  25236  bddmulibl  25348  ellimc2  25386  ellimc3  25388  limcflf  25390  limcresi  25394  limciun  25403  dvreslem  25418  dvres2lem  25419  dvres3a  25423  cpnres  25446  dvaddbr  25447  dvmulbr  25448  dvmptres3  25465  lhop1lem  25522  rlimcnp2  26461  xrlimcnp  26463  chpchtsum  26712  2sqlem8  26919  2sqlem9  26920  rpvmasumlem  26980  rplogsum  27020  dirith2  27021  nosupbnd2  27209  axtgsegcon  27705  axtg5seg  27706  axtgbtwnid  27707  axtgpasch  27708  axtgcont1  27709  tglng  27787  chdmm1i  30718  chm0i  30731  ledii  30777  lejdii  30779  pjoml2i  30826  pjoml4i  30828  cmcmlem  30832  cmbr4i  30842  osumcori  30884  pjssmii  30922  mayete3i  30969  riesz4  31305  riesz1  31306  cnlnadjeu  31319  nmopadjlei  31329  pjclem1  31436  pjci  31441  mdbr3  31538  mdbr4  31539  dmdbr2  31544  dmdbr5  31549  ssmd2  31553  mdslj1i  31560  mdslj2i  31561  mdsl1i  31562  mdsl2bi  31564  mdslmd1lem1  31566  mdslmd1lem2  31567  mdslmd2i  31571  csmdsymi  31575  cvexchlem  31609  atomli  31623  atcvat4i  31638  inindif  31742  difininv  31743  disjxpin  31807  imadifxp  31820  off2  31854  mptiffisupp  31903  resspos  32124  resstos  32125  submomnd  32216  suborng  32422  idlinsubrg  32538  ressply1evl  32636  evls1addd  32637  evls1muld  32638  evls1vsca  32639  ressply1invg  32647  evls1maprhm  32748  ordtrestNEW  32890  pnfneige0  32920  lmxrge0  32921  qqhnm  32959  qqhcn  32960  rrhre  32990  indsumin  33009  indf1ofs  33013  gsumesum  33046  esumlub  33047  esumcst  33050  esumpcvgval  33065  hasheuni  33072  esumcvg  33073  sigainb  33123  carsgclctunlem2  33307  sibfinima  33327  sibfof  33328  eulerpartlemelr  33345  eulerpartlemgh  33366  eulerpartlemgf  33367  eulerpartlemgs2  33368  eulerpartlemn  33369  probmeasb  33418  cndprob01  33423  hashreprin  33621  reprfi2  33624  breprexpnat  33635  hgt750lemd  33649  hgt750lema  33658  tgoldbachgtde  33661  tgoldbachgtda  33662  tgoldbachgt  33664  bnj1293  33816  connpconn  34215  iccllysconn  34230  cvmsss2  34254  cvmcov2  34255  cvmopnlem  34258  cvmliftmolem2  34262  cvmlift2lem12  34294  mvrsfpw  34486  elmsta  34528  msubvrs  34540  mclsind  34550  nepss  34676  dfon2lem4  34747  gg-dvmulbr  35164  trer  35190  neiin  35206  neibastop1  35233  neibastop2lem  35234  topmeet  35238  filnetlem3  35254  bj-disj2r  35898  bj-restpw  35962  bj-restb  35964  bj-restuni2  35968  bj-ablsscmn  36148  topdifinffinlem  36217  opnmbllem0  36513  mblfinlem4  36517  mbfposadd  36524  heibor1lem  36666  heiborlem1  36668  heiborlem3  36670  heiborlem10  36677  opidonOLD  36709  disjimin  37610  lshpinN  37848  lcvexchlem1  37893  lcvexchlem5  37897  pmod1i  38708  pmodN  38710  osumcllem7N  38822  pexmidlem4N  38833  dochdmj1  40250  dochexmidlem4  40323  lcfrlem25  40427  mapd1o  40508  mapdin  40522  elrfi  41418  elrfirn  41419  fnwe2lem2  41779  aomclem2  41783  lsmfgcl  41802  lmhmfgima  41812  lmhmfgsplit  41814  lmhmlnmsplit  41815  hbt  41858  ofoafg  42090  trrelind  42402  iunrelexp0  42439  isotone2  42786  grumnudlem  43030  ismnushort  43046  onfrALTlem3  43291  onfrALTlem2  43293  onfrALTlem3VD  43634  onfrALTlem2VD  43636  iunconnlem2  43682  restuni6  43797  disjinfi  43877  inmap  43894  dmresss  43919  fsumiunss  44278  islptre  44322  sumnnodd  44333  limcresiooub  44345  limcresioolb  44346  limcleqr  44347  limclner  44354  limclr  44358  limsuplesup  44402  limsuppnfdlem  44404  limsupres  44408  liminfgord  44457  liminfgf  44461  liminfcl  44466  limsupresxr  44469  liminfresxr  44470  liminfval2  44471  liminflelimsuplem  44478  liminfvalxr  44486  icccncfext  44590  fourierdlem20  44830  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem76  44885  fourierdlem103  44912  fourierdlem104  44913  fourierdlem113  44922  fouriersw  44934  salgencntex  45046  sge0less  45095  sge0resplit  45109  sge0split  45112  sge0iunmptlemre  45118  sge0fodjrnlem  45119  caragencmpl  45238  ovolval2lem  45346  ovolval2  45347  ovolval3  45350  ovolval4lem2  45353  sssmf  45441  fcoreslem4  45763  fcoresf1  45766  fcoresfo  45768  lidlssbas  46737  rnghmresfn  46815  rnghmsscmap  46826  rngchomrnghmresALTV  46848  rhmresfn  46861  rhmsscmap  46872  rhmsubclem4  46941