Theorem inss1 4159

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
inss1	⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Proof of Theorem inss1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elinel1 4125	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3921	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Syntax hints:   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  inss2  4160  ssinss1  4168  unabs  4185  nssinpss  4187  dfin4  4198  inv1  4325  disjdif  4402  ifssun  4473  uniintsn  4915  wefrc  5574  relin1  5711  resss  5905  resmpt3  5935  cnvcnvss  6086  resdmss  6127  resssxp  6162  predss  6199  ordtri3or  6283  onfr  6290  ordelinel  6349  funin  6494  funimass2  6501  fnresin1  6541  fnres  6543  fresin  6627  fresaun  6629  nfvres  6792  ssimaex  6835  fneqeql2  6906  fnfvimad  7092  funiunfv  7103  isoini2  7190  ofrfvalg  7519  ofval  7522  ofrval  7523  off  7529  ofres  7530  ofco  7534  fparlem3  7925  fparlem4  7926  frrlem4  8076  frrlem13  8085  smores  8154  smores2  8156  tfrlem5  8182  pmresg  8616  sbthlem7  8829  sbthcl  8835  infi  8972  imafiALT  9042  ixpfi2  9047  unifpw  9052  elfiun  9119  dffi3  9120  marypha1lem  9122  ordtypelem6  9212  ordtypelem7  9213  ordtypelem8  9214  wdomima2g  9275  frrlem15  9446  tskwe  9639  ackbij1lem15  9921  ackbij1lem16  9922  fin23lem23  10013  fin23lem22  10014  fin23lem19  10023  brdom3  10215  brdom5  10216  brdom4  10217  imadomg  10221  fpwwe2lem11  10328  canthp1lem2  10340  wunin  10400  tskin  10446  gruima  10489  ingru  10502  gruina  10505  grur1a  10506  nqerf  10617  nqerrel  10619  hashun3  14027  hashin  14054  hashdif  14056  xptrrel  14619  rexanuz  14985  limsupgle  15114  rlimres  15195  lo1res  15196  lo1resb  15201  rlimresb  15202  o1resb  15203  lo1eq  15205  rlimeq  15206  o1of2  15250  o1rlimmul  15256  isercolllem2  15305  isercolllem3  15306  isercoll  15307  incexclem  15476  incexc  15477  bitsinvp1  16084  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  sadasslem  16105  sadeq  16107  bitsres  16108  smuval2  16117  smupval  16123  smueqlem  16125  smumul  16128  ramub2  16643  ramub1lem2  16656  fvsetsid  16797  ressinbas  16881  ressress  16884  submre  17231  isacs1i  17283  mreacs  17284  acsfn  17285  invss  17390  sscres  17452  catcisolem  17741  catciso  17742  isacs5lem  18178  psss  18213  tsrss  18222  tsrdir  18237  sylow2a  19139  lsmmod  19196  gsumzres  19425  gsumzaddlem  19437  dprddisj2  19557  ablfac1eu  19591  isunit  19814  acsfn1p  19982  lspextmo  20233  2idlval  20417  pjfval  20823  pjpm  20825  aspsubrg  20990  psrbagsn  21181  ofco2  21508  basdif0  22011  tgval2  22014  eltg3  22020  tgcl  22027  tgdom  22036  tgidm  22038  ppttop  22065  epttop  22067  ntropn  22108  ntrin  22120  mretopd  22151  neiptoptop  22190  restfpw  22238  neitr  22239  restcls  22240  cncls  22333  cnpresti  22347  cnprest  22348  cmpsublem  22458  cmpsub  22459  fiuncmp  22463  indisconn  22477  connsub  22480  iunconnlem  22486  islly2  22543  cldllycmp  22554  kgentopon  22597  ptbasfi  22640  ptcnplem  22680  txcnmpt  22683  txcmplem2  22701  hausdiag  22704  txkgen  22711  xkococnlem  22718  qtoptop2  22758  basqtop  22770  fbssfi  22896  filin  22913  infil  22922  fbasrn  22943  fgtr  22949  ufprim  22968  flimrest  23042  txflf  23065  fclsrest  23083  alexsubALTlem4  23109  tsmsres  23203  tsmsxplem1  23212  ustund  23281  trust  23289  utoptop  23294  restutop  23297  cfiluweak  23355  xmetres  23425  metres  23426  blin2  23490  setsmstopn  23539  metrest  23586  ressxms  23587  tgioo  23865  xrsmopn  23881  reconnlem1  23895  xrge0tsms  23903  tcphcph  24306  cfilresi  24364  cfilres  24365  caussi  24366  causs  24367  relcmpcmet  24387  minveclem4a  24499  ismbl2  24596  cmmbl  24603  nulmbl2  24605  unmbl  24606  shftmbl  24607  volinun  24615  voliunlem1  24619  voliunlem2  24620  ioombl1lem4  24630  ioombl1  24631  uniioombllem2  24652  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombl  24658  volivth  24676  vitalilem3  24679  vitalilem4  24680  vitalilem5  24681  vitali  24682  mbfadd  24730  mbfsub  24731  i1fadd  24764  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  itg1climres  24784  mbfmul  24796  itg2splitlem  24818  itg2split  24819  limcresi  24954  limciun  24963  dvreslem  24978  dvres2lem  24979  dvres  24980  dvres3a  24983  dvaddbr  25007  dvmulbr  25008  dvfsumle  25090  dvfsumabs  25092  ig1peu  25241  pilem2  25516  pilem3  25517  rlimcnp2  26021  ppisval  26158  ppifi  26160  ppiprm  26205  chtprm  26207  chtdif  26212  efchtdvds  26213  ppidif  26217  ppiltx  26231  prmorcht  26232  ppiub  26257  chtlepsi  26259  pclogsum  26268  vmasum  26269  chpval2  26271  chpub  26273  2sqlem8  26479  chebbnd1lem1  26522  chtppilimlem1  26526  rpvmasum2  26565  dchrisum0re  26566  rplogsum  26580  dirith2  26581  axtgcgrrflx  26727  axtgcgrid  26728  axtgsegcon  26729  axtg5seg  26730  axtgbtwnid  26731  axtgpasch  26732  axtgcont1  26733  phnv  29077  minvecolem2  29138  minvecolem3  29139  minvecolem5  29144  minvecolem6  29145  minvecolem7  29146  hlimcaui  29499  chdmm1i  29740  chabs1  29779  chabs2  29780  ledii  29799  lejdii  29801  pjoml4i  29850  cmbr3i  29863  cmbr4i  29864  cmm1i  29869  osumcor2i  29907  3oalem4  29928  pjssmii  29944  pjocini  29961  pjini  29962  mayete3i  29991  riesz4  30327  riesz1  30328  cnlnadjeui  30340  cnlnadjeu  30341  cnlnssadj  30343  nmopadjlei  30351  pjin1i  30455  pjclem1  30458  stji1i  30505  stm1i  30506  dmdbr2  30566  ssmd1  30574  mdslj2i  30583  mdsl2bi  30586  mdslmd1lem1  30588  mdslmd2i  30593  atomli  30645  atcvat4i  30660  sumdmdlem2  30682  dmdbr5ati  30685  dmdbr6ati  30686  dmdbr7ati  30687  indifbi  30769  disjxpin  30828  imadifxp  30841  nfpconfp  30868  off2  30879  ffsrn  30966  gsummptres  31214  xrge0tsmsd  31219  idlinsubrg  31510  ordtrestNEW  31773  qqhnm  31840  qqhcn  31841  rrhre  31871  indsumin  31890  indf1ofs  31894  esumval  31914  esumel  31915  gsumesum  31927  esumlub  31928  esumcst  31931  esumfsup  31938  esumpcvgval  31946  esumcvg  31954  sigainb  32004  ldgenpisyslem1  32031  measinb2  32091  sibfinima  32206  sibfof  32207  eulerpartlemelr  32224  eulerpartlem1  32234  eulerpartgbij  32239  eulerpartlemgu  32244  eulerpartlemgs2  32247  sseqf  32259  ballotlemfelz  32357  ballotlemfp1  32358  reprinrn  32498  reprinfz1  32502  hgt750lemd  32528  bnj1292  32695  connpconn  33097  iccllysconn  33112  cvmsss2  33136  cvmcov2  33137  cvmopnlem  33140  cvmliftmolem2  33144  cvmliftlem15  33160  cvmlift2lem12  33176  mvrsfpw  33368  msrf  33404  elmsta  33410  mthmpps  33444  nepss  33564  dfon2lem4  33668  nosupbnd1lem1  33838  nosupbnd2  33846  noinfbnd1lem1  33853  txpss3v  34107  fixssdm  34135  fixssrn  34136  limitssson  34140  fneer  34469  neibastop1  34475  neibastop2lem  34476  filnetlem3  34496  ontopbas  34544  bj-disj2r  35145  bj-restpw  35190  bj-discrmoore  35209  bj-idres  35258  bj-fvsnun2  35354  bj-ablssgrp  35374  bj-fldssdrng  35386  taupilemrplb  35418  taupilem2  35420  taupi  35421  ptrest  35703  poimirlem29  35733  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  mbfposadd  35751  sstotbnd2  35859  ssbnd  35873  heibor1lem  35894  heiborlem1  35896  heiborlem3  35898  heiborlem5  35900  heiborlem6  35901  heiborlem10  35905  heibor  35906  opidonOLD  35937  exidcl  35961  flddivrng  36084  iss2  36406  xrnss3v  36429  refrelsredund2  36673  lshpinN  36930  lcvexchlem5  36979  pmodlem2  37788  pmod1i  37789  pmodN  37791  osumcllem7N  37903  pexmidlem4N  37914  pl42lem3N  37922  djaclN  39077  dihoml4c  39317  dochdmj1  39331  djhcl  39341  dochexmidlem4  39404  mapd1o  39589  mapdin  39603  elrfi  40432  elrfirn  40433  elrfirn2  40434  ismrcd1  40436  istopclsd  40438  isnacs2  40444  mrefg3  40446  isnacs3  40448  diophrw  40497  diophin  40510  aomclem2  40796  islmodfg  40810  lsmfgcl  40815  lmhmfgima  40825  lmhmfgsplit  40827  lmhmlnmsplit  40828  pwfi2f1o  40837  hbt  40871  harval3  41041  elinintrab  41074  trrelind  41162  clsk3nimkb  41539  isotone2  41548  ismnushort  41808  onfrALTlem2  42055  onfrALTlem2VD  42398  unirestss  42562  inmap  42638  fsumiunss  43006  islptre  43050  sumnnodd  43061  limclner  43082  liminfval4  43220  liminfval3  43221  cnrefiisplem  43260  cncfuni  43317  ismbl3  43417  ismbl4  43424  fouriersw  43662  qndenserrnbllem  43725  salincl  43754  salgencntex  43772  sge0less  43820  sge0resplit  43834  sge0split  43837  sge0iunmptlemre  43843  carageniuncllem1  43949  carageniuncllem2  43950  caragenel2d  43960  hspmbllem3  44056  hspmbl  44057  ovolval2lem  44071  sssmf  44161  smfaddlem1  44185  smflimlem2  44194  smflimlem3  44195  smflimlem4  44196  smfres  44211  smfmullem4  44215  smfsuplem1  44231  fcoreslem2  44445  rngcbas  45411  rngchomfval  45412  rngccofval  45416  dfrngc2  45418  rnghmsscmap2  45419  rnghmsscmap  45420  rngcsect  45426  funcrngcsetc  45444  ringcbas  45457  ringchomfval  45458  ringccofval  45462  dfringc2  45464  rhmsscmap2  45465  rhmsscmap  45466  rhmsscrnghm  45472  ringcsect  45477  funcringcsetc  45481  funcringcsetcALTV2lem9  45490  fldc  45529  fldhmsubc  45530  rngcrescrhm  45531  rhmsubclem1  45532  fldcALTV  45547  fldhmsubcALTV  45548  rngcrescrhmALTV  45549  rhmsubcALTVlem1  45550  iscnrm3llem2  46132  setrec2fun  46284