Theorem inss2 3796

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 3767	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3795	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstr3i 3599	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  difin0  3993  iunxdif3  4542  relin2  5160  relres  5346  ssrnres  5491  cnvcnv  5505  ordin  5670  onfr  5680  ordelinel  5742  ordelinelOLD  5743  fnresin2  5920  fresaunres2  5989  ssimaex  6173  exfo  6285  ffvresb  6301  ofrfval  6803  ofval  6804  ofrval  6805  off  6810  ofres  6811  ofco  6815  offres  7054  fnwelem  7179  fnse  7181  tpostpos  7259  wfrlem4  7305  smores3  7337  tfrlem5  7363  erinxp  7708  pmresg  7771  nnfi  8038  ixpfi2  8147  f1opwfi  8153  dffi2  8212  elfiun  8219  marypha1lem  8222  ordtypelem3  8308  ordtypelem6  8311  ordtypelem7  8312  hartogslem1  8330  unxpwdom  8377  epfrs  8490  tcmin  8500  bnd2  8639  tskwe  8659  r0weon  8718  infxpenlem  8719  fodomfi2  8766  infpwfien  8768  cdainf  8897  ackbij1lem6  8930  ackbij1lem9  8933  ackbij1lem10  8934  ackbij1lem11  8935  ackbij1lem15  8939  ackbij1lem16  8940  ackbij1lem18  8942  ackbij1b  8944  sdom2en01  9007  fin23lem26  9030  fin23lem13  9037  isfin1-3  9091  fin56  9098  fin1a2lem9  9113  ttukeylem6  9219  brdom3  9231  brdom5  9232  brdom4  9233  fpwwe2lem8  9338  fpwwe2lem9  9339  fpwwe2lem12  9342  fpwwe2  9344  canthwelem  9351  gruima  9503  ingru  9516  gruina  9519  grur1a  9520  ltrelpi  9590  ltrelnq  9627  nqerf  9631  dedekindle  10080  fzfi  12633  xptrrel  13567  rexanuz  13933  limsupgord  14051  limsupcl  14052  limsupgf  14054  limsupgle  14056  rlimres  14137  lo1res  14138  o1of2  14191  o1rlimmul  14197  ackbijnn  14399  bitsinv1  15002  bitsinvp1  15009  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  sadasslem  15030  sadeq  15032  smuval2  15042  smupval  15048  smueqlem  15050  prmrec  15464  isstruct2  15704  structcnvcnv  15706  ressbasss  15759  ressress  15765  restsspw  15915  pwsle  15975  submre  16088  isacs2  16137  isacs1i  16141  sscres  16306  rescabs  16316  resscat  16335  funcres2c  16384  coffth  16419  rescfth  16420  ressffth  16421  catccatid  16575  catcisolem  16579  catciso  16580  catcoppccl  16581  catcfuccl  16582  catcxpccl  16670  yoniso  16748  isdrs2  16762  isacs3lem  16989  acsinfd  17003  acsdomd  17004  psssdm2  17038  tsrss  17046  idrespermg  17654  mvdco  17688  sylow2a  17857  lsmmod  17911  frgpnabllem2  18100  subrgpropd  18637  lssacs  18788  sralmod  19008  asplss  19150  ressmplbas  19277  subrgmpl  19281  opsrtoslem2  19306  mplind  19323  ressply1bas  19420  pf1rcl  19534  zringlpirlem2  19652  zringlpirlem3  19653  ofco2  20076  basdif0  20568  eltg4i  20575  ntrss2  20671  ntrin  20675  isopn3  20680  mreclatdemoBAD  20710  neiptoptop  20745  restbas  20772  resttopon  20775  restuni2  20781  restcld  20786  restfpw  20793  neitr  20794  ordtrest  20816  subbascn  20868  cnrest2r  20901  cnpresti  20902  cnprest  20903  lmss  20912  cnrmi  20974  restcnrm  20976  resthauslem  20977  fincmp  21006  imacmp  21010  fiuncmp  21017  cmpfi  21021  bwth  21023  cnconn  21035  iuncon  21041  clscon  21043  concompclo  21048  1stcrest  21066  subislly  21094  islly2  21097  cldllycmp  21108  hauspwdom  21114  kgeni  21150  llycmpkgen2  21163  1stckgenlem  21166  ptbasfi  21194  txcls  21217  ptclsg  21228  txcnp  21233  ptcnplem  21234  txtube  21253  txcmplem1  21254  txcmplem2  21255  txkgen  21265  xkopt  21268  xkococnlem  21272  txcon  21302  basqtop  21324  tgqtop  21325  kqdisj  21345  kqnrmlem1  21356  kqnrmlem2  21357  nrmhmph  21407  infil  21477  fbasrn  21498  trfg  21505  uzrest  21511  isufil2  21522  fmfnfmlem4  21571  hauspwpwf1  21601  txflf  21620  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem2  21667  tmdgsum2  21710  tsmsres  21757  tsmsxplem1  21766  ustexsym  21829  ustund  21835  trust  21843  utoptop  21848  restutop  21851  blres  22046  met2ndci  22137  metrest  22139  restmetu  22185  tgioo  22407  zdis  22427  reconnlem2  22438  reconn  22439  cnheibor  22562  lebnum  22571  cphsqrtcl  22792  tchcph  22844  cfilresi  22901  cfilres  22902  caussi  22903  causs  22904  minveclem4b  23010  minveclem4  23011  ovolfcl  23042  ovolfioo  23043  ovolficc  23044  ovolficcss  23045  ovolfsval  23046  ovolfsf  23047  ovollb  23054  ovoliunlem1  23077  ovolicc2lem1  23092  ovolicc2lem2  23093  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicc2  23097  nulmbl  23110  voliunlem1  23125  ioombl1lem4  23136  ovolfs2  23145  uniiccdif  23152  uniioovol  23153  uniiccvol  23154  uniioombllem2a  23156  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombllem6  23162  uniioombl  23163  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  volcn  23180  volivth  23181  vitalilem2  23184  vitalilem4  23186  mbfadd  23234  mbfsub  23235  i1fima  23251  i1fima2  23252  i1fd  23254  i1fadd  23268  i1fmul  23269  itg1addlem2  23270  itg1addlem4  23272  itg1addlem5  23273  i1fres  23278  mbfmul  23299  bddmulibl  23411  ellimc2  23447  ellimc3  23449  limcflf  23451  limcresi  23455  limciun  23464  dvreslem  23479  dvres2lem  23480  dvres3a  23484  cpnres  23506  dvaddbr  23507  dvmulbr  23508  dvmptres3  23525  lhop1lem  23580  ig1peu  23735  taylfvallem1  23915  rlimcnp2  24493  xrlimcnp  24495  ppisval  24630  chtf  24634  efchtcl  24637  chtge0  24638  ppinprm  24678  chtprm  24679  chtnprm  24680  chtwordi  24682  chtdif  24684  efchtdvds  24685  chtlepsi  24731  chtleppi  24735  pclogsum  24740  chpval2  24743  chpchtsum  24744  chpub  24745  2sqlem8  24951  2sqlem9  24952  chebbnd1lem1  24958  chtppilimlem1  24962  rplogsumlem2  24974  rpvmasumlem  24976  rplogsum  25016  dirith2  25017  axtgsegcon  25163  axtg5seg  25164  axtgbtwnid  25165  axtgpasch  25166  axtgcont1  25167  tglng  25241  perpneq  25409  ragperp  25412  chdmm1i  27720  chm0i  27733  ledii  27779  lejdii  27781  pjoml2i  27828  pjoml4i  27830  cmcmlem  27834  cmbr4i  27844  osumcori  27886  pjssmii  27924  mayete3i  27971  riesz4  28307  riesz1  28308  cnlnadjeu  28321  nmopadjlei  28331  pjclem1  28438  pjci  28443  mdbr3  28540  mdbr4  28541  dmdbr2  28546  dmdbr5  28551  ssmd2  28555  mdslj1i  28562  mdslj2i  28563  mdsl1i  28564  mdsl2bi  28566  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd2i  28573  csmdsymi  28577  cvexchlem  28611  atomli  28625  atcvat4i  28640  inindif  28738  disjin2  28782  disjxpin  28783  imadifxp  28796  off2  28823  partfun  28858  resspos  28990  resstos  28991  submomnd  29041  suborng  29146  prsdm  29288  prsrn  29289  ordtrestNEW  29295  pnfneige0  29325  lmxrge0  29326  qqhnm  29362  qqhcn  29363  rrhre  29393  indf1ofs  29415  gsumesum  29448  esumlub  29449  esumcst  29452  esumpcvgval  29467  hasheuni  29474  esumcvg  29475  sigainb  29526  carsgclctunlem2  29708  sibfinima  29728  sibfof  29729  eulerpartlemelr  29746  eulerpartlemgh  29767  eulerpartlemgf  29768  eulerpartlemgs2  29769  eulerpartlemn  29770  probmeasb  29819  cndprob01  29824  bnj1293  30141  conpcon  30471  iccllyscon  30486  cvmsss2  30510  cvmcov2  30511  cvmopnlem  30514  cvmliftmolem2  30518  cvmlift2lem12  30550  mvrsfpw  30657  elmsta  30699  msubvrs  30711  mclsind  30721  nepss  30854  elrn3  30906  dfon2lem4  30935  frrlem4  31027  trer  31480  neiin  31497  neibastop1  31524  neibastop2lem  31525  topmeet  31529  filnetlem3  31545  bj-restpw  32226  bj-restb  32228  bj-restuni2  32232  bj-ablsscmn  32317  topdifinffinlem  32371  opnmbllem0  32615  mblfinlem4  32619  mbfposadd  32627  heibor1lem  32778  heiborlem1  32780  heiborlem3  32782  heiborlem10  32789  opidonOLD  32821  lshpinN  33294  lcvexchlem1  33339  lcvexchlem5  33343  pmod1i  34152  pmodN  34154  osumcllem7N  34266  pexmidlem4N  34277  dochdmj1  35697  dochexmidlem4  35770  lcfrlem25  35874  mapd1o  35955  mapdin  35969  elrfi  36275  elrfirn  36276  fnwe2lem2  36639  aomclem2  36643  lsmfgcl  36662  lmhmfgima  36672  lmhmfgsplit  36674  lmhmlnmsplit  36675  hbt  36719  acsfn1p  36788  trrelind  36976  iunrelexp0  37013  isotone2  37367  onfrALTlem3  37780  onfrALTlem2  37782  onfrALTlem3VD  38145  onfrALTlem2VD  38147  iunconlem2  38193  restuni6  38337  disjinfi  38375  inmap  38396  fsumiunss  38642  islptre  38686  sumnnodd  38697  limcresiooub  38709  limcresioolb  38710  limcleqr  38711  limclner  38718  limclr  38722  icccncfext  38773  fourierdlem20  39020  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem76  39075  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  fouriersw  39124  salgencntex  39237  sge0less  39285  sge0resplit  39299  sge0split  39302  sge0iunmptlemre  39308  sge0fodjrnlem  39309  caragencmpl  39425  ovolval2lem  39533  ovolval2  39534  ovolval3  39537  ovolval4lem2  39540  sssmf  39625  lidlssbas  41712  rnghmresfn  41755  rnghmsscmap  41766  rngchomrnghmresALTV  41788  rhmresfn  41801  rhmsscmap  41812  rhmsubclem4  41881