Theorem inss2 4259

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 4230	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4258	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 4044	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  difin0  4497  iunxdif3  5118  relin2  5837  relres  6035  idssxp  6078  ssrnres  6209  cnvrescnv  6226  ordin  6425  onfr  6434  ordelinel  6496  fnresin2  6706  fresaunres2  6793  ssimaex  7007  exfo  7139  ffvresb  7159  fnfvimad  7271  ofrfvalg  7722  ofval  7725  ofrval  7726  off  7732  ofres  7733  ofco  7738  fnwelem  8172  fnse  8174  fprlem1  8341  tfrlem5  8436  pmresg  8928  nnfiOLD  9295  ixpfi2  9420  elfiun  9499  marypha1lem  9502  ordtypelem6  9592  ordtypelem7  9593  hartogslem1  9611  unxpwdom  9658  epfrs  9800  tcmin  9810  bnd2  9962  tskwe  10019  r0weon  10081  infxpenlem  10082  djuinf  10258  ackbij1lem9  10296  ackbij1lem10  10297  ackbij1lem15  10302  ackbij1lem16  10303  ackbij1b  10307  sdom2en01  10371  fin23lem26  10394  fin23lem13  10401  isfin1-3  10455  fin56  10462  fin1a2lem9  10477  brdom3  10597  brdom5  10598  brdom4  10599  fpwwe2lem11  10710  fpwwe2  10712  canthwelem  10719  gruima  10871  ingru  10884  gruina  10887  grur1a  10888  ltrelpi  10958  ltrelnq  10995  nqerf  10999  fzfi  14023  xptrrel  15029  rexanuz  15394  limsupgord  15518  limsupcl  15519  limsupgf  15521  limsupgle  15523  o1of2  15659  o1rlimmul  15665  ackbijnn  15876  bitsinv1  16488  bitsinvp1  16495  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  smupval  16534  prmrec  16969  structcnvcnv  17200  ressbasss  17297  ressbasssOLD  17298  ressress  17307  restsspw  17491  submre  17663  isacs1i  17715  rescabs  17896  rescabsOLD  17897  resscat  17916  funcres2c  17968  ressffth  18005  catccatid  18173  catcisolem  18177  catciso  18178  yoniso  18355  acsinfd  18626  acsdomd  18627  tsrss  18659  idresefmnd  18934  idrespermg  19453  mvdco  19487  lsmmod  19717  rnghmresfn  20641  rnghmsscmap  20652  rhmresfn  20670  rhmsscmap  20681  rhmsubclem4  20710  acsfn1p  20822  lssacs  20988  lidlssbas  21246  zringlpirlem2  21497  zringlpirlem3  21498  asplss  21917  ressmplbas  22069  subrgmpl  22073  mplind  22117  ressply1bas  22251  pf1rcl  22374  ressply1evl  22395  evls1addd  22396  evls1muld  22397  evls1vsca  22398  evls1maprhm  22401  ofco2  22478  basdif0  22981  eltg4i  22988  ntrss2  23086  ntrin  23090  isopn3  23095  resttopon  23190  restuni2  23196  restcld  23201  restfpw  23208  neitr  23209  cnrest2r  23316  cnpresti  23317  cnprest  23318  lmss  23327  cnrmi  23389  restcnrm  23391  resthauslem  23392  imacmp  23426  fiuncmp  23433  subislly  23510  islly2  23513  cldllycmp  23524  hauspwdom  23530  kgeni  23566  llycmpkgen2  23579  ptbasfi  23610  ptclsg  23644  ptcnplem  23650  txtube  23669  txcmplem2  23671  txkgen  23681  kqdisj  23761  fbasrn  23913  trfg  23920  isufil2  23937  fmfnfmlem4  23986  hauspwpwf1  24016  txflf  24035  alexsubALTlem4  24079  tmdgsum2  24125  tsmsres  24173  tsmsxplem1  24182  ustexsym  24245  ustund  24251  trust  24259  utoptop  24264  restutop  24267  metrest  24558  restmetu  24604  tgioo  24837  reconnlem2  24868  cphsqrtcl  25237  tcphcph  25290  cfilresi  25348  caussi  25350  causs  25351  ovolfioo  25521  ovolficc  25522  ovolficcss  25523  ovolfsf  25525  ovollb  25533  ovolicc2lem1  25571  ovolicc2lem2  25572  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2  25576  nulmbl  25589  voliunlem1  25604  ovolfs2  25625  uniiccdif  25632  uniioovol  25633  uniiccvol  25634  uniioombllem2  25637  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  uniioombllem6  25642  uniioombl  25643  dyadmbllem  25653  dyadmbl  25654  opnmbllem  25655  volcn  25660  volivth  25661  mbfadd  25715  mbfsub  25716  i1fima  25732  i1fima2  25733  i1fd  25735  i1fadd  25749  i1fmul  25750  itg1addlem2  25751  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  i1fres  25760  mbfmul  25781  bddmulibl  25894  ellimc2  25932  ellimc3  25934  limcflf  25936  limcresi  25940  limciun  25949  dvreslem  25964  dvres2lem  25965  dvres3a  25969  cpnres  25993  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvmptres3  26014  lhop1lem  26072  rlimcnp2  27027  xrlimcnp  27029  chpchtsum  27281  2sqlem8  27488  2sqlem9  27489  rpvmasumlem  27549  rplogsum  27589  dirith2  27590  nosupbnd2  27779  axtgsegcon  28490  axtg5seg  28491  axtgbtwnid  28492  axtgpasch  28493  axtgcont1  28494  tglng  28572  chdmm1i  31509  chm0i  31522  ledii  31568  lejdii  31570  pjoml2i  31617  pjoml4i  31619  cmcmlem  31623  cmbr4i  31633  osumcori  31675  pjssmii  31713  mayete3i  31760  riesz4  32096  riesz1  32097  cnlnadjeu  32110  nmopadjlei  32120  pjclem1  32227  pjci  32232  mdbr3  32329  mdbr4  32330  dmdbr2  32335  dmdbr5  32340  ssmd2  32344  mdslj1i  32351  mdslj2i  32352  mdsl1i  32353  mdsl2bi  32355  mdslmd1lem1  32357  mdslmd1lem2  32358  mdslmd2i  32362  csmdsymi  32366  cvexchlem  32400  atomli  32414  atcvat4i  32429  inindif  32546  difininv  32547  disjxpin  32610  imadifxp  32623  off2  32660  mptiffisupp  32705  resspos  32939  resstos  32940  submomnd  33060  suborng  33310  idlinsubrg  33424  ressply1invg  33559  evls1subd  33562  algextdeglem7  33714  algextdeglem8  33715  ordtrestNEW  33867  pnfneige0  33897  lmxrge0  33898  qqhnm  33936  qqhcn  33937  rrhre  33967  indsumin  33986  indf1ofs  33990  gsumesum  34023  esumlub  34024  esumcst  34027  esumpcvgval  34042  hasheuni  34049  esumcvg  34050  sigainb  34100  carsgclctunlem2  34284  sibfinima  34304  sibfof  34305  eulerpartlemelr  34322  eulerpartlemgh  34343  eulerpartlemgf  34344  eulerpartlemgs2  34345  eulerpartlemn  34346  probmeasb  34395  cndprob01  34400  hashreprin  34597  reprfi2  34600  breprexpnat  34611  hgt750lemd  34625  hgt750lema  34634  tgoldbachgtde  34637  tgoldbachgtda  34638  tgoldbachgt  34640  bnj1293  34792  connpconn  35203  iccllysconn  35218  cvmsss2  35242  cvmcov2  35243  cvmopnlem  35246  cvmliftmolem2  35250  cvmlift2lem12  35282  mvrsfpw  35474  elmsta  35516  msubvrs  35528  mclsind  35538  nepss  35680  dfon2lem4  35750  trer  36282  neiin  36298  neibastop1  36325  neibastop2lem  36326  topmeet  36330  filnetlem3  36346  weiunfr  36433  bj-disj2r  36994  bj-restpw  37058  bj-restb  37060  bj-restuni2  37064  bj-ablsscmn  37244  topdifinffinlem  37313  opnmbllem0  37616  mblfinlem4  37620  mbfposadd  37627  heibor1lem  37769  heiborlem1  37771  heiborlem3  37773  heiborlem10  37780  opidonOLD  37812  disjimin  38707  lshpinN  38945  lcvexchlem1  38990  lcvexchlem5  38994  pmod1i  39805  pmodN  39807  osumcllem7N  39919  pexmidlem4N  39930  dochdmj1  41347  dochexmidlem4  41420  lcfrlem25  41524  mapd1o  41605  mapdin  41619  elrfi  42650  elrfirn  42651  fnwe2lem2  43008  aomclem2  43012  lsmfgcl  43031  lmhmfgima  43041  lmhmfgsplit  43043  lmhmlnmsplit  43044  hbt  43087  ofoafg  43316  trrelind  43627  iunrelexp0  43664  isotone2  44011  grumnudlem  44254  ismnushort  44270  onfrALTlem3  44515  onfrALTlem2  44517  onfrALTlem3VD  44858  onfrALTlem2VD  44860  iunconnlem2  44906  restuni6  45024  disjinfi  45099  inmap  45116  fsumiunss  45496  islptre  45540  sumnnodd  45551  limcresiooub  45563  limcresioolb  45564  limcleqr  45565  limclner  45572  limclr  45576  limsuplesup  45620  limsuppnfdlem  45622  limsupres  45626  liminfgord  45675  liminfgf  45679  liminfcl  45684  limsupresxr  45687  liminfresxr  45688  liminfval2  45689  liminflelimsuplem  45696  liminfvalxr  45704  icccncfext  45808  fourierdlem20  46048  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem76  46103  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  fouriersw  46152  salgencntex  46264  sge0less  46313  sge0resplit  46327  sge0split  46330  sge0iunmptlemre  46336  sge0fodjrnlem  46337  caragencmpl  46456  ovolval2lem  46564  ovolval2  46565  ovolval3  46568  ovolval4lem2  46571  sssmf  46659  fcoreslem4  46981  fcoresf1  46984  fcoresfo  46986  3f1oss1  46990  rngchomrnghmresALTV  48002