Theorem inss2 4190

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 4162	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4189	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstrri 3985	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

This proof depends on syntax axioms:   ∩ cin 3905   ⊆ wss 3906

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923

This theorem is used by:  inindif  4331  vvin  4366  difin0  4435  uniin  4898  iunxdif3  5063  relin2  5802  relres  6006  idssxp  6053  rnin  6145  ssrnres  6178  cnvrescnv  6196  ordin  6395  onfr  6404  ordelinel  6468  fnresin2  6665  fresaunres2  6754  ssimaex  6970  exfo  7104  ffvresb  7125  fnfvimad  7236  ofrfvalg  7688  ofval  7691  ofrval  7692  off  7698  ofres  7699  ofco  7705  fnwelem  8129  fnse  8131  fprlem1  8299  tfrlem5  8368  pmresg  8870  ixpfi2  9310  elfiun  9393  marypha1lem  9396  ordtypelem6  9488  ordtypelem7  9489  hartogslem1  9507  unxpwdom  9554  epfrs  9703  tcmin  9711  bnd2  9888  tskwe  9948  r0weon  10008  infxpenlem  10009  djuinf  10184  ackbij1lem9  10222  ackbij1lem10  10223  ackbij1lem15  10228  ackbij1lem16  10229  ackbij1b  10233  sdom2en01  10297  fin23lem26  10320  fin23lem13  10327  isfin1-3  10381  fin56  10388  fin1a2lem9  10403  brdom3  10523  brdom5  10524  brdom4  10525  fpwwe2lem11  10637  fpwwe2  10639  canthwelem  10646  gruima  10798  ingru  10811  gruina  10814  grur1a  10815  ltrelpi  10885  ltrelnq  10922  nqerf  10926  fzfi  14022  xptrrel  15037  rexanuz  15417  limsupgord  15543  limsupcl  15544  limsupgf  15546  limsupgle  15548  o1of2  15684  o1rlimmul  15690  ackbijnn  15901  bitsinv1  16518  bitsinvp1  16525  sadcaddlem  16533  sadadd2lem  16535  sadadd3  16537  sadaddlem  16542  sadasslem  16546  sadeq  16548  smupval  16564  prmrec  17000  structcnvcnv  17231  ressbasss  17317  ressbasssOLD  17318  ressress  17325  restsspw  17502  submre  17675  isacs1i  17731  rescabs  17908  resscat  17927  funcres2c  17978  ressffth  18015  catccatid  18181  catcisolem  18185  catciso  18186  yoniso  18359  resspos  18503  resstos  18504  acsinfd  18630  acsdomd  18631  tsrss  18663  idresefmnd  18982  idrespermg  19505  mvdco  19539  lsmmod  19769  submomnd  20226  rnghmresfn  20748  rnghmsscmap  20759  rhmresfn  20777  rhmsscmap  20788  rhmsubclem4  20817  acsfn1p  20932  suborng  21009  lssacs  21118  lidlssbas  21368  zringlpirlem2  21643  zringlpirlem3  21644  asplss  22053  ressmplbas  22208  subrgmpl  22212  mplind  22251  ressply1bas  22418  pf1rcl  22539  ressply1evl  22560  evls1addd  22561  evls1muld  22562  evls1vsca  22563  evls1maprhm  22566  ofco2  22638  basdif0  23140  eltg4i  23147  ntrss2  23244  ntrin  23248  isopn3  23253  resttopon  23348  restuni2  23354  restcld  23359  restfpw  23366  neitr  23367  cnrest2r  23474  cnpresti  23475  cnprest  23476  lmss  23485  cnrmi  23547  restcnrm  23549  resthauslem  23550  imacmp  23584  fiuncmp  23591  subislly  23669  islly2  23672  cldllycmp  23683  hauspwdom  23689  kgeni  23725  llycmpkgen2  23738  ptbasfi  23769  ptclsg  23803  ptcnplem  23809  txtube  23828  txcmplem2  23830  txkgen  23840  kqdisj  23920  fbasrn  24072  trfg  24079  isufil2  24096  fmfnfmlem4  24145  hauspwpwf1  24175  txflf  24194  alexsubALTlem4  24238  tmdgsum2  24284  tsmsres  24332  tsmsxplem1  24341  ustexsym  24404  ustund  24410  trust  24417  utoptop  24422  restutop  24425  metrest  24712  restmetu  24758  tgioo  24984  reconnlem2  25016  cphsqrtcl  25374  tcphcph  25427  cfilresi  25485  caussi  25487  causs  25488  ovolfioo  25657  ovolficc  25658  ovolficcss  25659  ovolfsf  25661  ovollb  25669  ovolicc2lem1  25707  ovolicc2lem2  25708  ovolicc2lem3  25709  ovolicc2lem4  25710  ovolicc2  25712  nulmbl  25725  voliunlem1  25740  ovolfs2  25761  uniiccdif  25768  uniioovol  25769  uniiccvol  25770  uniioombllem2  25773  uniioombllem3a  25774  uniioombllem3  25775  uniioombllem4  25776  uniioombllem5  25777  uniioombllem6  25778  uniioombl  25779  dyadmbllem  25789  dyadmbl  25790  opnmbllem  25791  volcn  25796  volivth  25797  mbfadd  25851  mbfsub  25852  i1fima  25868  i1fima2  25869  i1fd  25871  i1fadd  25885  i1fmul  25886  itg1addlem2  25887  itg1addlem4  25889  itg1addlem5  25890  i1fres  25895  mbfmul  25916  bddmulibl  26029  ellimc2  26067  ellimc3  26069  limcflf  26071  limcresi  26075  limciun  26084  dvreslem  26099  dvres2lem  26100  dvres3a  26104  cpnres  26127  dvaddbr  26128  dvmulbr  26129  dvmptres3  26146  lhop1lem  26203  rlimcnp2  27162  xrlimcnp  27164  chpchtsum  27414  2sqlem8  27621  2sqlem9  27622  rpvmasumlem  27682  rplogsum  27722  dirith2  27723  nosupbnd2  27911  axtgsegcon  28764  axtg5seg  28765  axtgbtwnid  28766  axtgpasch  28767  axtgcont1  28768  tglng  28846  chdmm1i  31876  chm0i  31889  ledii  31935  lejdii  31937  pjoml2i  31984  pjoml4i  31986  cmcmlem  31990  cmbr4i  32000  osumcori  32042  pjssmii  32080  mayete3i  32127  riesz4  32463  riesz1  32464  cnlnadjeu  32477  nmopadjlei  32487  pjclem1  32594  pjci  32599  mdbr3  32696  mdbr4  32697  dmdbr2  32702  dmdbr5  32707  ssmd2  32711  mdslj1i  32718  mdslj2i  32719  mdsl1i  32720  mdsl2bi  32722  mdslmd1lem1  32724  mdslmd1lem2  32725  mdslmd2i  32729  csmdsymi  32733  cvexchlem  32767  atomli  32781  atcvat4i  32796  difininv  32910  disjxpin  32980  imadifxp  32993  off2  33033  mptiffisupp  33085  indsumin  33227  indf1ofs  33232  idlinsubrg  33779  ressply1invg  33899  evls1subd  33902  algextdeglem7  34153  algextdeglem8  34154  ordtrestNEW  34351  pnfneige0  34381  lmxrge0  34382  qqhnm  34420  qqhcn  34421  rrhre  34451  gsumesum  34489  esumlub  34490  esumcst  34493  esumpcvgval  34508  hasheuni  34515  esumcvg  34516  sigainb  34567  carsgclctunlem2  34750  sibfinima  34770  sibfof  34771  eulerpartlemelr  34788  eulerpartlemgh  34809  eulerpartlemgf  34810  eulerpartlemgs2  34811  eulerpartlemn  34812  probmeasb  34861  cndprob01  34866  hashreprin  35048  reprfi2  35051  breprexpnat  35062  hgt750lemd  35076  hgt750lema  35085  tgoldbachgtde  35088  tgoldbachgtda  35089  tgoldbachgt  35091  bnj1293  35245  connpconn  35740  iccllysconn  35755  cvmsss2  35779  cvmcov2  35780  cvmopnlem  35783  cvmliftmolem2  35787  cvmlift2lem12  35819  mvrsfpw  36011  elmsta  36053  msubvrs  36065  mclsind  36075  nepss  36223  dfon2lem4  36289  trer  36860  neiin  36876  neibastop1  36903  neibastop2lem  36904  topmeet  36908  filnetlem3  36924  weiunfr  37011  elttcirr  37075  bj-disj2r  37697  bj-restpw  37767  bj-restb  37769  bj-restuni2  37773  bj-ablsscmn  37955  topdifinffinlem  38026  opnmbllem0  38340  mblfinlem4  38344  mbfposadd  38351  heibor1lem  38493  heiborlem1  38495  heiborlem3  38497  heiborlem10  38504  opidonOLD  38536  disjimin  39533  lshpinN  39796  lcvexchlem1  39841  lcvexchlem5  39845  pmod1i  40655  pmodN  40657  osumcllem7N  40769  pexmidlem4N  40780  dochdmj1  42197  dochexmidlem4  42270  lcfrlem25  42374  mapd1o  42455  mapdin  42469  elrfi  43458  elrfirn  43459  fnwe2lem2  43811  aomclem2  43815  lsmfgcl  43834  lmhmfgima  43844  lmhmfgsplit  43846  lmhmlnmsplit  43847  hbt  43890  ofoafg  44114  trrelind  44424  iunrelexp0  44461  isotone2  44808  grumnudlem  45028  ismnushort  45044  onfrALTlem3  45286  onfrALTlem2  45288  onfrALTlem3VD  45628  onfrALTlem2VD  45630  iunconnlem2  45676  wfac8prim  45744  restuni6  45873  disjinfi  45943  inmap  45958  fsumiunss  46324  islptre  46368  sumnnodd  46379  limcresiooub  46389  limcresioolb  46390  limcleqr  46391  limclner  46398  limclr  46402  limsuplesup  46446  limsuppnfdlem  46448  limsupres  46452  liminfgord  46501  liminfgf  46505  liminfcl  46510  limsupresxr  46513  liminfresxr  46514  liminfval2  46515  liminflelimsuplem  46522  liminfvalxr  46530  icccncfext  46634  fourierdlem20  46874  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  fourierdlem76  46929  fourierdlem103  46956  fourierdlem104  46957  fourierdlem113  46966  fouriersw  46978  salgencntex  47090  sge0less  47139  sge0resplit  47153  sge0split  47156  sge0iunmptlemre  47162  sge0fodjrnlem  47163  caragencmpl  47282  ovolval2lem  47390  ovolval2  47391  ovolval3  47394  ovolval4lem2  47397  sssmf  47485  nthrucw  47640  fcoreslem4  47836  fcoresf1  47839  fcoresfo  47841  3f1oss1  47845  rngchomrnghmresALTV  49077  termc  50330