Theorem inss2 4054

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 4028	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 4053	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstr3i 3855	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3791   ⊆ wss 3792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-ss 3806

This theorem is referenced by:  difin0  4265  iunxdif3  4842  relin2  5486  relres  5677  idssxp  5712  ssrnres  5828  ordin  6008  onfr  6017  ordelinel  6076  fnresin2  6254  fresaunres2  6328  ssimaex  6525  exfo  6643  ffvresb  6660  fnfvimad  6768  ofrfval  7184  ofval  7185  ofrval  7186  off  7191  ofres  7192  ofco  7196  fnwelem  7575  fnse  7577  wfrlem4OLD  7703  tfrlem5  7761  pmresg  8170  nnfi  8443  ixpfi2  8554  elfiun  8626  marypha1lem  8629  ordtypelem6  8719  ordtypelem7  8720  hartogslem1  8738  unxpwdom  8785  epfrs  8906  tcmin  8916  bnd2  9055  tskwe  9111  r0weon  9170  infxpenlem  9171  cdainf  9351  ackbij1lem9  9387  ackbij1lem10  9388  ackbij1lem15  9393  ackbij1lem16  9394  ackbij1b  9398  sdom2en01  9461  fin23lem26  9484  fin23lem13  9491  isfin1-3  9545  fin56  9552  fin1a2lem9  9567  brdom3  9687  brdom5  9688  brdom4  9689  fpwwe2lem12  9800  fpwwe2  9802  canthwelem  9809  gruima  9961  ingru  9974  gruina  9977  grur1a  9978  ltrelpi  10048  ltrelnq  10085  nqerf  10089  fzfi  13095  xptrrel  14134  rexanuz  14499  limsupgord  14620  limsupcl  14621  limsupgf  14623  limsupgle  14625  o1of2  14760  o1rlimmul  14766  ackbijnn  14973  bitsinv1  15580  bitsinvp1  15587  sadcaddlem  15595  sadadd2lem  15597  sadadd3  15599  sadaddlem  15604  sadasslem  15608  sadeq  15610  smupval  15626  prmrec  16041  structcnvcnv  16280  ressbasss  16339  ressress  16346  restsspw  16489  submre  16662  isacs1i  16714  rescabs  16889  resscat  16908  funcres2c  16957  ressffth  16994  catccatid  17148  catcisolem  17152  catciso  17153  yoniso  17322  acsinfd  17577  acsdomd  17578  tsrss  17620  idrespermg  18225  mvdco  18259  sylow2a  18429  lsmmod  18483  lssacs  19373  asplss  19737  ressmplbas  19864  subrgmpl  19868  mplind  19909  ressply1bas  20006  pf1rcl  20120  zringlpirlem2  20240  zringlpirlem3  20241  ofco2  20673  basdif0  21176  eltg4i  21183  ntrss2  21280  ntrin  21284  isopn3  21289  resttopon  21384  restuni2  21390  restcld  21395  restfpw  21402  neitr  21403  cnrest2r  21510  cnpresti  21511  cnprest  21512  lmss  21521  cnrmi  21583  restcnrm  21585  resthauslem  21586  imacmp  21620  fiuncmp  21627  subislly  21704  islly2  21707  cldllycmp  21718  hauspwdom  21724  kgeni  21760  llycmpkgen2  21773  ptbasfi  21804  ptclsg  21838  ptcnplem  21844  txtube  21863  txcmplem2  21865  txkgen  21875  kqdisj  21955  fbasrn  22107  trfg  22114  isufil2  22131  fmfnfmlem4  22180  hauspwpwf1  22210  txflf  22229  alexsubALTlem4  22273  tmdgsum2  22319  tsmsres  22366  tsmsxplem1  22375  ustexsym  22438  ustund  22444  trust  22452  utoptop  22457  restutop  22460  metrest  22748  restmetu  22794  tgioo  23018  reconnlem2  23049  cphsqrtcl  23402  tcphcph  23454  cfilresi  23512  caussi  23514  causs  23515  minveclem4b  23648  minveclem4  23649  ovolfcl  23681  ovolfioo  23682  ovolficc  23683  ovolficcss  23684  ovolfsval  23685  ovolfsf  23686  ovollb  23694  ovolicc2lem1  23732  ovolicc2lem2  23733  ovolicc2lem3  23734  ovolicc2lem4  23735  ovolicc2lem5  23736  ovolicc2  23737  nulmbl  23750  voliunlem1  23765  ioombl1lem4  23776  ovolfs2  23786  uniiccdif  23793  uniioovol  23794  uniiccvol  23795  uniioombllem2a  23797  uniioombllem2  23798  uniioombllem3a  23799  uniioombllem3  23800  uniioombllem4  23801  uniioombllem5  23802  uniioombllem6  23803  uniioombl  23804  dyadmbllem  23814  dyadmbl  23815  opnmbllem  23816  volcn  23821  volivth  23822  vitalilem2  23824  vitalilem4  23826  mbfadd  23876  mbfsub  23877  i1fima  23893  i1fima2  23894  i1fd  23896  i1fadd  23910  i1fmul  23911  itg1addlem2  23912  itg1addlem4  23914  itg1addlem5  23915  i1fres  23920  mbfmul  23941  bddmulibl  24053  ellimc2  24089  ellimc3  24091  limcflf  24093  limcresi  24097  limciun  24106  dvreslem  24121  dvres2lem  24122  dvres3a  24126  cpnres  24148  dvaddbr  24149  dvmulbr  24150  dvmptres3  24167  lhop1lem  24224  ig1peu  24379  taylfvallem1  24559  rlimcnp2  25156  xrlimcnp  25158  ppisval  25293  chtf  25297  efchtcl  25300  chtge0  25301  ppinprm  25341  chtprm  25342  chtnprm  25343  chtwordi  25345  chtdif  25347  efchtdvds  25348  chtlepsi  25394  chtleppi  25398  pclogsum  25403  chpval2  25406  chpchtsum  25407  chpub  25408  2sqlem8  25614  2sqlem9  25615  chebbnd1lem1  25627  chtppilimlem1  25631  rplogsumlem2  25643  rpvmasumlem  25645  rplogsum  25685  dirith2  25686  axtgsegcon  25832  axtg5seg  25833  axtgbtwnid  25834  axtgpasch  25835  axtgcont1  25836  tglng  25914  perpneq  26082  ragperp  26085  chdmm1i  28925  chm0i  28938  ledii  28984  lejdii  28986  pjoml2i  29033  pjoml4i  29035  cmcmlem  29039  cmbr4i  29049  osumcori  29091  pjssmii  29129  mayete3i  29176  riesz4  29512  riesz1  29513  cnlnadjeu  29526  nmopadjlei  29536  pjclem1  29643  pjci  29648  mdbr3  29745  mdbr4  29746  dmdbr2  29751  dmdbr5  29756  ssmd2  29760  mdslj1i  29767  mdslj2i  29768  mdsl1i  29769  mdsl2bi  29771  mdslmd1lem1  29773  mdslmd1lem2  29774  mdslmd2i  29778  csmdsymi  29782  cvexchlem  29816  atomli  29830  atcvat4i  29845  inindif  29932  difininv  29933  disjxpin  29981  imadifxp  29994  off2  30025  resspos  30229  resstos  30230  submomnd  30280  suborng  30385  prsdm  30566  prsrn  30567  ordtrestNEW  30573  pnfneige0  30603  lmxrge0  30604  qqhnm  30640  qqhcn  30641  rrhre  30671  indsumin  30690  indf1ofs  30694  gsumesum  30727  esumlub  30728  esumcst  30731  esumpcvgval  30746  hasheuni  30753  esumcvg  30754  sigainb  30805  carsgclctunlem2  30987  sibfinima  31007  sibfof  31008  eulerpartlemelr  31025  eulerpartlemgh  31046  eulerpartlemgf  31047  eulerpartlemgs2  31048  eulerpartlemn  31049  probmeasb  31099  cndprob01  31104  hashreprin  31308  reprfi2  31311  breprexpnat  31322  hgt750lemd  31336  hgt750lema  31345  tgoldbachgtde  31348  tgoldbachgtda  31349  tgoldbachgt  31351  bnj1293  31494  connpconn  31824  iccllysconn  31839  cvmsss2  31863  cvmcov2  31864  cvmopnlem  31867  cvmliftmolem2  31871  cvmlift2lem12  31903  mvrsfpw  32010  elmsta  32052  msubvrs  32064  mclsind  32074  nepss  32204  elrn3  32254  dfon2lem4  32287  nosupbnd2  32459  trer  32907  neiin  32923  neibastop1  32950  neibastop2lem  32951  topmeet  32955  filnetlem3  32971  bj-disj2r  33593  bj-restpw  33626  bj-restb  33628  bj-restuni2  33632  bj-ablsscmn  33749  topdifinffinlem  33797  opnmbllem0  34080  mblfinlem4  34084  mbfposadd  34091  heibor1lem  34241  heiborlem1  34243  heiborlem3  34245  heiborlem10  34252  opidonOLD  34284  lshpinN  35152  lcvexchlem1  35197  lcvexchlem5  35201  pmod1i  36011  pmodN  36013  osumcllem7N  36125  pexmidlem4N  36136  dochdmj1  37553  dochexmidlem4  37626  lcfrlem25  37730  mapd1o  37811  mapdin  37825  elrfi  38231  elrfirn  38232  fnwe2lem2  38594  aomclem2  38598  lsmfgcl  38617  lmhmfgima  38627  lmhmfgsplit  38629  lmhmlnmsplit  38630  hbt  38673  acsfn1p  38742  trrelind  38928  iunrelexp0  38965  isotone2  39317  onfrALTlem3  39718  onfrALTlem2  39720  onfrALTlem3VD  40070  onfrALTlem2VD  40072  iunconnlem2  40118  restuni6  40248  disjinfi  40317  inmap  40336  dmresss  40367  fnfvima2  40403  fsumiunss  40729  islptre  40773  sumnnodd  40784  limcresiooub  40796  limcresioolb  40797  limcleqr  40798  limclner  40805  limclr  40809  limsuplesup  40853  limsuppnfdlem  40855  limsupres  40859  liminfgord  40908  liminfgf  40912  liminfcl  40917  limsupresxr  40920  liminfresxr  40921  liminfval2  40922  liminflelimsuplem  40929  liminfvalxr  40937  icccncfext  41042  fourierdlem20  41285  fourierdlem48  41312  fourierdlem49  41313  fourierdlem50  41314  fourierdlem76  41340  fourierdlem103  41367  fourierdlem104  41368  fourierdlem113  41377  fouriersw  41389  salgencntex  41499  sge0less  41547  sge0resplit  41561  sge0split  41564  sge0iunmptlemre  41570  sge0fodjrnlem  41571  caragencmpl  41690  ovolval2lem  41798  ovolval2  41799  ovolval3  41802  ovolval4lem2  41805  sssmf  41888  lidlssbas  42951  rnghmresfn  42992  rnghmsscmap  43003  rngchomrnghmresALTV  43025  rhmresfn  43038  rhmsscmap  43049  rhmsubclem4  43118