Theorem inss2 4206

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 4178	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4205	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 4002	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3935   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  difin0  4422  iunxdif3  5017  relin2  5686  relres  5882  idssxp  5916  ssrnres  6035  cnvrescnv  6052  ordin  6221  onfr  6230  ordelinel  6289  fnresin2  6473  fresaunres2  6550  ssimaex  6748  exfo  6871  ffvresb  6888  fnfvimad  6996  ofrfval  7417  ofval  7418  ofrval  7419  off  7424  ofres  7425  ofco  7429  fnwelem  7825  fnse  7827  tfrlem5  8016  pmresg  8434  nnfi  8711  ixpfi2  8822  elfiun  8894  marypha1lem  8897  ordtypelem6  8987  ordtypelem7  8988  hartogslem1  9006  unxpwdom  9053  epfrs  9173  tcmin  9183  bnd2  9322  tskwe  9379  r0weon  9438  infxpenlem  9439  djuinf  9614  ackbij1lem9  9650  ackbij1lem10  9651  ackbij1lem15  9656  ackbij1lem16  9657  ackbij1b  9661  sdom2en01  9724  fin23lem26  9747  fin23lem13  9754  isfin1-3  9808  fin56  9815  fin1a2lem9  9830  brdom3  9950  brdom5  9951  brdom4  9952  fpwwe2lem12  10063  fpwwe2  10065  canthwelem  10072  gruima  10224  ingru  10237  gruina  10240  grur1a  10241  ltrelpi  10311  ltrelnq  10348  nqerf  10352  fzfi  13341  xptrrel  14340  rexanuz  14705  limsupgord  14829  limsupcl  14830  limsupgf  14832  limsupgle  14834  o1of2  14969  o1rlimmul  14975  ackbijnn  15183  bitsinv1  15791  bitsinvp1  15798  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  sadasslem  15819  sadeq  15821  smupval  15837  prmrec  16258  structcnvcnv  16497  ressbasss  16556  ressress  16562  restsspw  16705  submre  16876  isacs1i  16928  rescabs  17103  resscat  17122  funcres2c  17171  ressffth  17208  catccatid  17362  catcisolem  17366  catciso  17367  yoniso  17535  acsinfd  17790  acsdomd  17791  tsrss  17833  idresefmnd  18064  idrespermg  18539  mvdco  18573  sylow2a  18744  lsmmod  18801  acsfn1p  19578  lssacs  19739  asplss  20103  ressmplbas  20237  subrgmpl  20241  mplind  20282  ressply1bas  20397  pf1rcl  20512  zringlpirlem2  20632  zringlpirlem3  20633  ofco2  21060  basdif0  21561  eltg4i  21568  ntrss2  21665  ntrin  21669  isopn3  21674  resttopon  21769  restuni2  21775  restcld  21780  restfpw  21787  neitr  21788  cnrest2r  21895  cnpresti  21896  cnprest  21897  lmss  21906  cnrmi  21968  restcnrm  21970  resthauslem  21971  imacmp  22005  fiuncmp  22012  subislly  22089  islly2  22092  cldllycmp  22103  hauspwdom  22109  kgeni  22145  llycmpkgen2  22158  ptbasfi  22189  ptclsg  22223  ptcnplem  22229  txtube  22248  txcmplem2  22250  txkgen  22260  kqdisj  22340  fbasrn  22492  trfg  22499  isufil2  22516  fmfnfmlem4  22565  hauspwpwf1  22595  txflf  22614  alexsubALTlem4  22658  tmdgsum2  22704  tsmsres  22752  tsmsxplem1  22761  ustexsym  22824  ustund  22830  trust  22838  utoptop  22843  restutop  22846  metrest  23134  restmetu  23180  tgioo  23404  reconnlem2  23435  cphsqrtcl  23788  tcphcph  23840  cfilresi  23898  caussi  23900  causs  23901  ovolfioo  24068  ovolficc  24069  ovolficcss  24070  ovolfsf  24072  ovollb  24080  ovolicc2lem1  24118  ovolicc2lem2  24119  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2  24123  nulmbl  24136  voliunlem1  24151  ovolfs2  24172  uniiccdif  24179  uniioovol  24180  uniiccvol  24181  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombllem6  24189  uniioombl  24190  dyadmbllem  24200  dyadmbl  24201  opnmbllem  24202  volcn  24207  volivth  24208  mbfadd  24262  mbfsub  24263  i1fima  24279  i1fima2  24280  i1fd  24282  i1fadd  24296  i1fmul  24297  itg1addlem2  24298  itg1addlem4  24300  itg1addlem5  24301  i1fres  24306  mbfmul  24327  bddmulibl  24439  ellimc2  24475  ellimc3  24477  limcflf  24479  limcresi  24483  limciun  24492  dvreslem  24507  dvres2lem  24508  dvres3a  24512  cpnres  24534  dvaddbr  24535  dvmulbr  24536  dvmptres3  24553  lhop1lem  24610  rlimcnp2  25544  xrlimcnp  25546  chpchtsum  25795  2sqlem8  26002  2sqlem9  26003  rpvmasumlem  26063  rplogsum  26103  dirith2  26104  axtgsegcon  26250  axtg5seg  26251  axtgbtwnid  26252  axtgpasch  26253  axtgcont1  26254  tglng  26332  chdmm1i  29254  chm0i  29267  ledii  29313  lejdii  29315  pjoml2i  29362  pjoml4i  29364  cmcmlem  29368  cmbr4i  29378  osumcori  29420  pjssmii  29458  mayete3i  29505  riesz4  29841  riesz1  29842  cnlnadjeu  29855  nmopadjlei  29865  pjclem1  29972  pjci  29977  mdbr3  30074  mdbr4  30075  dmdbr2  30080  dmdbr5  30085  ssmd2  30089  mdslj1i  30096  mdslj2i  30097  mdsl1i  30098  mdsl2bi  30100  mdslmd1lem1  30102  mdslmd1lem2  30103  mdslmd2i  30107  csmdsymi  30111  cvexchlem  30145  atomli  30159  atcvat4i  30174  inindif  30278  difininv  30279  disjxpin  30338  imadifxp  30351  off2  30388  resspos  30646  resstos  30647  submomnd  30711  suborng  30888  ordtrestNEW  31164  pnfneige0  31194  lmxrge0  31195  qqhnm  31231  qqhcn  31232  rrhre  31262  indsumin  31281  indf1ofs  31285  gsumesum  31318  esumlub  31319  esumcst  31322  esumpcvgval  31337  hasheuni  31344  esumcvg  31345  sigainb  31395  carsgclctunlem2  31577  sibfinima  31597  sibfof  31598  eulerpartlemelr  31615  eulerpartlemgh  31636  eulerpartlemgf  31637  eulerpartlemgs2  31638  eulerpartlemn  31639  probmeasb  31688  cndprob01  31693  hashreprin  31891  reprfi2  31894  breprexpnat  31905  hgt750lemd  31919  hgt750lema  31928  tgoldbachgtde  31931  tgoldbachgtda  31932  tgoldbachgt  31934  bnj1293  32088  connpconn  32482  iccllysconn  32497  cvmsss2  32521  cvmcov2  32522  cvmopnlem  32525  cvmliftmolem2  32529  cvmlift2lem12  32561  mvrsfpw  32753  elmsta  32795  msubvrs  32807  mclsind  32817  nepss  32948  dfon2lem4  33031  fprlem1  33137  nosupbnd2  33216  trer  33664  neiin  33680  neibastop1  33707  neibastop2lem  33708  topmeet  33712  filnetlem3  33728  bj-disj2r  34343  bj-restpw  34386  bj-restb  34388  bj-restuni2  34392  bj-ablsscmn  34563  topdifinffinlem  34631  opnmbllem0  34943  mblfinlem4  34947  mbfposadd  34954  heibor1lem  35102  heiborlem1  35104  heiborlem3  35106  heiborlem10  35113  opidonOLD  35145  disjimin  35996  lshpinN  36140  lcvexchlem1  36185  lcvexchlem5  36189  pmod1i  36999  pmodN  37001  osumcllem7N  37113  pexmidlem4N  37124  dochdmj1  38541  dochexmidlem4  38614  lcfrlem25  38718  mapd1o  38799  mapdin  38813  elrfi  39340  elrfirn  39341  fnwe2lem2  39700  aomclem2  39704  lsmfgcl  39723  lmhmfgima  39733  lmhmfgsplit  39735  lmhmlnmsplit  39736  hbt  39779  trrelind  40059  iunrelexp0  40096  isotone2  40448  grumnudlem  40670  onfrALTlem3  40927  onfrALTlem2  40929  onfrALTlem3VD  41270  onfrALTlem2VD  41272  iunconnlem2  41318  restuni6  41437  disjinfi  41503  inmap  41521  dmresss  41550  fsumiunss  41905  islptre  41949  sumnnodd  41960  limcresiooub  41972  limcresioolb  41973  limcleqr  41974  limclner  41981  limclr  41985  limsuplesup  42029  limsuppnfdlem  42031  limsupres  42035  liminfgord  42084  liminfgf  42088  liminfcl  42093  limsupresxr  42096  liminfresxr  42097  liminfval2  42098  liminflelimsuplem  42105  liminfvalxr  42113  icccncfext  42219  fourierdlem20  42461  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem76  42516  fourierdlem103  42543  fourierdlem104  42544  fourierdlem113  42553  fouriersw  42565  salgencntex  42675  sge0less  42723  sge0resplit  42737  sge0split  42740  sge0iunmptlemre  42746  sge0fodjrnlem  42747  caragencmpl  42866  ovolval2lem  42974  ovolval2  42975  ovolval3  42978  ovolval4lem2  42981  sssmf  43064  lidlssbas  44242  rnghmresfn  44283  rnghmsscmap  44294  rngchomrnghmresALTV  44316  rhmresfn  44329  rhmsscmap  44340  rhmsubclem4  44409