Theorem inss2 3834

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 3805	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inss1 3833	. 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
3	1, 2	eqsstr3i 3636	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵

Syntax hints:   ∩ cin 3573   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  difin0  4041  iunxdif3  4606  relin2  5237  relres  5426  ssrnres  5572  cnvcnv  5586  cnvcnvOLD  5587  ordin  5753  onfr  5763  ordelinel  5825  ordelinelOLD  5826  fnresin2  6006  fresaunres2  6076  ssimaex  6263  exfo  6377  ffvresb  6394  ofrfval  6905  ofval  6906  ofrval  6907  off  6912  ofres  6913  ofco  6917  offres  7163  fnwelem  7292  fnse  7294  tpostpos  7372  wfrlem4  7418  smores3  7450  tfrlem5  7476  erinxp  7821  pmresg  7885  nnfi  8153  ixpfi2  8264  f1opwfi  8270  dffi2  8329  elfiun  8336  marypha1lem  8339  ordtypelem3  8425  ordtypelem6  8428  ordtypelem7  8429  hartogslem1  8447  unxpwdom  8494  epfrs  8607  tcmin  8617  bnd2  8756  tskwe  8776  r0weon  8835  infxpenlem  8836  fodomfi2  8883  infpwfien  8885  cdainf  9014  ackbij1lem6  9047  ackbij1lem9  9050  ackbij1lem10  9051  ackbij1lem11  9052  ackbij1lem15  9056  ackbij1lem16  9057  ackbij1lem18  9059  ackbij1b  9061  sdom2en01  9124  fin23lem26  9147  fin23lem13  9154  isfin1-3  9208  fin56  9215  fin1a2lem9  9230  ttukeylem6  9336  brdom3  9350  brdom5  9351  brdom4  9352  fpwwe2lem8  9459  fpwwe2lem9  9460  fpwwe2lem12  9463  fpwwe2  9465  canthwelem  9472  gruima  9624  ingru  9637  gruina  9640  grur1a  9641  ltrelpi  9711  ltrelnq  9748  nqerf  9752  dedekindle  10201  fzfi  12771  xptrrel  13719  rexanuz  14085  limsupgord  14203  limsupcl  14204  limsupgf  14206  limsupgle  14208  rlimres  14289  lo1res  14290  o1of2  14343  o1rlimmul  14349  ackbijnn  14560  bitsinv1  15164  bitsinvp1  15171  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  sadeq  15194  smuval2  15204  smupval  15210  smueqlem  15212  prmrec  15626  isstruct2  15867  structcnvcnv  15871  ressbasss  15932  ressress  15938  restsspw  16092  pwsle  16152  submre  16265  isacs2  16314  isacs1i  16318  sscres  16483  rescabs  16493  resscat  16512  funcres2c  16561  coffth  16596  rescfth  16597  ressffth  16598  catccatid  16752  catcisolem  16756  catciso  16757  catcoppccl  16758  catcfuccl  16759  catcxpccl  16847  yoniso  16925  isdrs2  16939  isacs3lem  17166  acsinfd  17180  acsdomd  17181  psssdm2  17215  tsrss  17223  idrespermg  17831  mvdco  17865  sylow2a  18034  lsmmod  18088  frgpnabllem2  18277  subrgpropd  18814  lssacs  18967  sralmod  19187  asplss  19329  ressmplbas  19456  subrgmpl  19460  opsrtoslem2  19485  mplind  19502  ressply1bas  19599  pf1rcl  19713  zringlpirlem2  19833  zringlpirlem3  19834  ofco2  20257  basdif0  20757  eltg4i  20764  ntrss2  20861  ntrin  20865  isopn3  20870  mreclatdemoBAD  20900  neiptoptop  20935  restbas  20962  resttopon  20965  restuni2  20971  restcld  20976  restfpw  20983  neitr  20984  ordtrest  21006  subbascn  21058  cnrest2r  21091  cnpresti  21092  cnprest  21093  lmss  21102  cnrmi  21164  restcnrm  21166  resthauslem  21167  fincmp  21196  imacmp  21200  fiuncmp  21207  cmpfi  21211  bwth  21213  cnconn  21225  iunconn  21231  clsconn  21233  conncompclo  21238  1stcrest  21256  subislly  21284  islly2  21287  cldllycmp  21298  hauspwdom  21304  kgeni  21340  llycmpkgen2  21353  1stckgenlem  21356  ptbasfi  21384  txcls  21407  ptclsg  21418  txcnp  21423  ptcnplem  21424  txtube  21443  txcmplem1  21444  txcmplem2  21445  txkgen  21455  xkopt  21458  xkococnlem  21462  txconn  21492  basqtop  21514  tgqtop  21515  kqdisj  21535  kqnrmlem1  21546  kqnrmlem2  21547  nrmhmph  21597  infil  21667  fbasrn  21688  trfg  21695  uzrest  21701  isufil2  21712  fmfnfmlem4  21761  hauspwpwf1  21791  txflf  21810  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem2  21857  tmdgsum2  21900  tsmsres  21947  tsmsxplem1  21956  ustexsym  22019  ustund  22025  trust  22033  utoptop  22038  restutop  22041  blres  22236  met2ndci  22327  metrest  22329  restmetu  22375  tgioo  22599  zdis  22619  reconnlem2  22630  reconn  22631  cnheibor  22754  lebnum  22763  cphsqrtcl  22984  tchcph  23036  cfilresi  23093  cfilres  23094  caussi  23095  causs  23096  minveclem4b  23202  minveclem4  23203  ovolfcl  23235  ovolfioo  23236  ovolficc  23237  ovolficcss  23238  ovolfsval  23239  ovolfsf  23240  ovollb  23247  ovoliunlem1  23270  ovolicc2lem1  23285  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicc2  23290  nulmbl  23303  voliunlem1  23318  ioombl1lem4  23329  ovolfs2  23339  uniiccdif  23346  uniioovol  23347  uniiccvol  23348  uniioombllem2a  23350  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombllem6  23356  uniioombl  23357  dyadmbllem  23367  dyadmbl  23368  opnmbllem  23369  volcn  23374  volivth  23375  vitalilem2  23378  vitalilem4  23380  mbfadd  23428  mbfsub  23429  i1fima  23445  i1fima2  23446  i1fd  23448  i1fadd  23462  i1fmul  23463  itg1addlem2  23464  itg1addlem4  23466  itg1addlem5  23467  i1fres  23472  mbfmul  23493  bddmulibl  23605  ellimc2  23641  ellimc3  23643  limcflf  23645  limcresi  23649  limciun  23658  dvreslem  23673  dvres2lem  23674  dvres3a  23678  cpnres  23700  dvaddbr  23701  dvmulbr  23702  dvmptres3  23719  lhop1lem  23776  ig1peu  23931  taylfvallem1  24111  rlimcnp2  24693  xrlimcnp  24695  ppisval  24830  chtf  24834  efchtcl  24837  chtge0  24838  ppinprm  24878  chtprm  24879  chtnprm  24880  chtwordi  24882  chtdif  24884  efchtdvds  24885  chtlepsi  24931  chtleppi  24935  pclogsum  24940  chpval2  24943  chpchtsum  24944  chpub  24945  2sqlem8  25151  2sqlem9  25152  chebbnd1lem1  25158  chtppilimlem1  25162  rplogsumlem2  25174  rpvmasumlem  25176  rplogsum  25216  dirith2  25217  axtgsegcon  25363  axtg5seg  25364  axtgbtwnid  25365  axtgpasch  25366  axtgcont1  25367  tglng  25441  perpneq  25609  ragperp  25612  chdmm1i  28336  chm0i  28349  ledii  28395  lejdii  28397  pjoml2i  28444  pjoml4i  28446  cmcmlem  28450  cmbr4i  28460  osumcori  28502  pjssmii  28540  mayete3i  28587  riesz4  28923  riesz1  28924  cnlnadjeu  28937  nmopadjlei  28947  pjclem1  29054  pjci  29059  mdbr3  29156  mdbr4  29157  dmdbr2  29162  dmdbr5  29167  ssmd2  29171  mdslj1i  29178  mdslj2i  29179  mdsl1i  29180  mdsl2bi  29182  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd2i  29189  csmdsymi  29193  cvexchlem  29227  atomli  29241  atcvat4i  29256  inindif  29353  difininv  29354  disjxpin  29401  imadifxp  29414  off2  29443  resspos  29659  resstos  29660  submomnd  29710  suborng  29815  prsdm  29960  prsrn  29961  ordtrestNEW  29967  pnfneige0  29997  lmxrge0  29998  qqhnm  30034  qqhcn  30035  rrhre  30065  indsumin  30084  indf1ofs  30088  gsumesum  30121  esumlub  30122  esumcst  30125  esumpcvgval  30140  hasheuni  30147  esumcvg  30148  sigainb  30199  carsgclctunlem2  30381  sibfinima  30401  sibfof  30402  eulerpartlemelr  30419  eulerpartlemgh  30440  eulerpartlemgf  30441  eulerpartlemgs2  30442  eulerpartlemn  30443  probmeasb  30492  cndprob01  30497  hashreprin  30698  reprfi2  30701  breprexpnat  30712  hgt750lemd  30726  hgt750lema  30735  tgoldbachgtde  30738  tgoldbachgtda  30739  tgoldbachgt  30741  bnj1293  30887  connpconn  31217  iccllysconn  31232  cvmsss2  31256  cvmcov2  31257  cvmopnlem  31260  cvmliftmolem2  31264  cvmlift2lem12  31296  mvrsfpw  31403  elmsta  31445  msubvrs  31457  mclsind  31467  nepss  31599  elrn3  31652  dfon2lem4  31691  frrlem4  31783  nosupbnd2  31862  trer  32310  neiin  32327  neibastop1  32354  neibastop2lem  32355  topmeet  32359  filnetlem3  32375  bj-disj2r  33013  bj-restpw  33045  bj-restb  33047  bj-restuni2  33051  bj-ablsscmn  33140  topdifinffinlem  33195  opnmbllem0  33445  mblfinlem4  33449  mbfposadd  33457  heibor1lem  33608  heiborlem1  33610  heiborlem3  33612  heiborlem10  33619  opidonOLD  33651  lshpinN  34276  lcvexchlem1  34321  lcvexchlem5  34325  pmod1i  35134  pmodN  35136  osumcllem7N  35248  pexmidlem4N  35259  dochdmj1  36679  dochexmidlem4  36752  lcfrlem25  36856  mapd1o  36937  mapdin  36951  elrfi  37257  elrfirn  37258  fnwe2lem2  37621  aomclem2  37625  lsmfgcl  37644  lmhmfgima  37654  lmhmfgsplit  37656  lmhmlnmsplit  37657  hbt  37700  acsfn1p  37769  trrelind  37957  iunrelexp0  37994  isotone2  38347  onfrALTlem3  38759  onfrALTlem2  38761  onfrALTlem3VD  39123  onfrALTlem2VD  39125  iunconnlem2  39171  restuni6  39305  disjinfi  39380  inmap  39401  dmresss  39436  fnfvimad  39459  fnfvima2  39478  fsumiunss  39807  islptre  39851  sumnnodd  39862  limcresiooub  39874  limcresioolb  39875  limcleqr  39876  limclner  39883  limclr  39887  limsuplesup  39931  limsuppnfdlem  39933  limsupres  39937  liminfgord  39986  liminfgf  39990  liminfcl  39995  limsupresxr  39998  liminfresxr  39999  liminfval2  40000  liminflelimsuplem  40007  liminfvalxr  40015  icccncfext  40100  fourierdlem20  40344  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem76  40399  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  fouriersw  40448  salgencntex  40561  sge0less  40609  sge0resplit  40623  sge0split  40626  sge0iunmptlemre  40632  sge0fodjrnlem  40633  caragencmpl  40749  ovolval2lem  40857  ovolval2  40858  ovolval3  40861  ovolval4lem2  40864  sssmf  40947  lidlssbas  41922  rnghmresfn  41963  rnghmsscmap  41974  rngchomrnghmresALTV  41996  rhmresfn  42009  rhmsscmap  42020  rhmsubclem4  42089