Theorem inss1 4133

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 4100	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3896	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Syntax hints:   ∩ cin 3857   ⊆ wss 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875

This theorem is referenced by:  inss2  4134  ssinss1  4142  unabs  4159  nssinpss  4161  dfin4  4172  inv1  4290  disjdif  4368  ifssun  4437  uniintsn  4877  wefrc  5518  relin1  5654  resss  5848  resmpt3  5878  cnvcnvss  6023  resdmss  6064  resssxp  6099  predss  6133  ordtri3or  6201  onfr  6208  ordelinel  6267  funin  6411  funimass2  6418  fnresin1  6455  fnres  6457  fresin  6532  fresaun  6534  nfvres  6694  ssimaex  6737  fneqeql2  6808  fnfvimad  6988  funiunfv  6999  isoini2  7086  ofrfvalg  7412  ofval  7415  ofrval  7416  off  7422  ofres  7423  ofco  7427  fparlem3  7814  fparlem4  7815  smores  7999  smores2  8001  tfrlem5  8026  pmresg  8452  sbthlem7  8655  sbthcl  8661  infi  8779  imafiOLD  8850  ixpfi2  8855  unifpw  8860  elfiun  8927  dffi3  8928  marypha1lem  8930  ordtypelem6  9020  ordtypelem7  9021  ordtypelem8  9022  wdomima2g  9083  tskwe  9412  ackbij1lem15  9694  ackbij1lem16  9695  fin23lem23  9786  fin23lem22  9787  fin23lem19  9796  brdom3  9988  brdom5  9989  brdom4  9990  imadomg  9994  fpwwe2lem11  10101  canthp1lem2  10113  wunin  10173  tskin  10219  gruima  10262  ingru  10275  gruina  10278  grur1a  10279  nqerf  10390  nqerrel  10392  hashun3  13795  hashin  13822  hashdif  13824  xptrrel  14387  rexanuz  14753  limsupgle  14882  rlimres  14963  lo1res  14964  lo1resb  14969  rlimresb  14970  o1resb  14971  lo1eq  14973  rlimeq  14974  o1of2  15017  o1rlimmul  15023  isercolllem2  15070  isercolllem3  15071  isercoll  15072  incexclem  15239  incexc  15240  bitsinvp1  15848  sadcaddlem  15856  sadadd2lem  15858  sadadd3  15860  sadaddlem  15865  sadasslem  15869  sadeq  15871  bitsres  15872  smuval2  15881  smupval  15887  smueqlem  15889  smumul  15892  ramub2  16405  ramub1lem2  16418  fvsetsid  16573  ressinbas  16618  ressress  16620  submre  16934  isacs1i  16986  mreacs  16987  acsfn  16988  invss  17090  sscres  17152  catcisolem  17432  catciso  17433  isacs5lem  17845  psss  17890  tsrss  17899  tsrdir  17914  sylow2a  18811  lsmmod  18868  gsumzres  19097  gsumzaddlem  19109  dprddisj2  19229  ablfac1eu  19263  isunit  19478  acsfn1p  19646  lspextmo  19896  2idlval  20074  pjfval  20471  pjpm  20473  aspsubrg  20638  psrbagsn  20824  ofco2  21151  basdif0  21653  tgval2  21656  eltg3  21662  tgcl  21669  tgdom  21678  tgidm  21680  ppttop  21707  epttop  21709  ntropn  21749  ntrin  21761  mretopd  21792  neiptoptop  21831  restfpw  21879  neitr  21880  restcls  21881  cncls  21974  cnpresti  21988  cnprest  21989  cmpsublem  22099  cmpsub  22100  fiuncmp  22104  indisconn  22118  connsub  22121  iunconnlem  22127  islly2  22184  cldllycmp  22195  kgentopon  22238  ptbasfi  22281  ptcnplem  22321  txcnmpt  22324  txcmplem2  22342  hausdiag  22345  txkgen  22352  xkococnlem  22359  qtoptop2  22399  basqtop  22411  fbssfi  22537  filin  22554  infil  22563  fbasrn  22584  fgtr  22590  ufprim  22609  flimrest  22683  txflf  22706  fclsrest  22724  alexsubALTlem4  22750  tsmsres  22844  tsmsxplem1  22853  ustund  22922  trust  22930  utoptop  22935  restutop  22938  cfiluweak  22996  xmetres  23066  metres  23067  blin2  23131  setsmstopn  23180  metrest  23226  ressxms  23227  tgioo  23497  xrsmopn  23513  reconnlem1  23527  xrge0tsms  23535  tcphcph  23937  cfilresi  23995  cfilres  23996  caussi  23997  causs  23998  relcmpcmet  24018  minveclem4a  24130  ismbl2  24227  cmmbl  24234  nulmbl2  24236  unmbl  24237  shftmbl  24238  volinun  24246  voliunlem1  24250  voliunlem2  24251  ioombl1lem4  24261  ioombl1  24262  uniioombllem2  24283  uniioombllem3  24285  uniioombllem4  24286  uniioombllem5  24287  uniioombl  24289  volivth  24307  vitalilem3  24310  vitalilem4  24311  vitalilem5  24312  vitali  24313  mbfadd  24361  mbfsub  24362  i1fadd  24395  itg1addlem2  24397  itg1addlem4  24399  itg1addlem5  24400  itg1climres  24414  mbfmul  24426  itg2splitlem  24448  itg2split  24449  limcresi  24584  limciun  24593  dvreslem  24608  dvres2lem  24609  dvres  24610  dvres3a  24613  dvaddbr  24637  dvmulbr  24638  dvfsumle  24720  dvfsumabs  24722  ig1peu  24871  pilem2  25146  pilem3  25147  rlimcnp2  25651  ppisval  25788  ppifi  25790  ppiprm  25835  chtprm  25837  chtdif  25842  efchtdvds  25843  ppidif  25847  ppiltx  25861  prmorcht  25862  ppiub  25887  chtlepsi  25889  pclogsum  25898  vmasum  25899  chpval2  25901  chpub  25903  2sqlem8  26109  chebbnd1lem1  26152  chtppilimlem1  26156  rpvmasum2  26195  dchrisum0re  26196  rplogsum  26210  dirith2  26211  axtgcgrrflx  26355  axtgcgrid  26356  axtgsegcon  26357  axtg5seg  26358  axtgbtwnid  26359  axtgpasch  26360  axtgcont1  26361  phnv  28696  minvecolem2  28757  minvecolem3  28758  minvecolem5  28763  minvecolem6  28764  minvecolem7  28765  hlimcaui  29118  chdmm1i  29359  chabs1  29398  chabs2  29399  ledii  29418  lejdii  29420  pjoml4i  29469  cmbr3i  29482  cmbr4i  29483  cmm1i  29488  osumcor2i  29526  3oalem4  29547  pjssmii  29563  pjocini  29580  pjini  29581  mayete3i  29610  riesz4  29946  riesz1  29947  cnlnadjeui  29959  cnlnadjeu  29960  cnlnssadj  29962  nmopadjlei  29970  pjin1i  30074  pjclem1  30077  stji1i  30124  stm1i  30125  dmdbr2  30185  ssmd1  30193  mdslj2i  30202  mdsl2bi  30205  mdslmd1lem1  30207  mdslmd2i  30212  atomli  30264  atcvat4i  30279  sumdmdlem2  30301  dmdbr5ati  30304  dmdbr6ati  30305  dmdbr7ati  30306  indifbi  30390  disjxpin  30449  imadifxp  30462  nfpconfp  30489  off2  30500  ffsrn  30588  gsummptres  30838  xrge0tsmsd  30843  idlinsubrg  31129  ordtrestNEW  31392  qqhnm  31459  qqhcn  31460  rrhre  31490  indsumin  31509  indf1ofs  31513  esumval  31533  esumel  31534  gsumesum  31546  esumlub  31547  esumcst  31550  esumfsup  31557  esumpcvgval  31565  esumcvg  31573  sigainb  31623  ldgenpisyslem1  31650  measinb2  31710  sibfinima  31825  sibfof  31826  eulerpartlemelr  31843  eulerpartlem1  31853  eulerpartgbij  31858  eulerpartlemgu  31863  eulerpartlemgs2  31866  sseqf  31878  ballotlemfelz  31976  ballotlemfp1  31977  reprinrn  32117  reprinfz1  32121  hgt750lemd  32147  bnj1292  32315  connpconn  32713  iccllysconn  32728  cvmsss2  32752  cvmcov2  32753  cvmopnlem  32756  cvmliftmolem2  32760  cvmliftlem15  32776  cvmlift2lem12  32792  mvrsfpw  32984  msrf  33020  elmsta  33026  mthmpps  33060  nepss  33180  dfon2lem4  33278  frrlem4  33387  frrlem13  33396  frrlem15  33403  nosupbnd1lem1  33476  nosupbnd2  33484  noinfbnd1lem1  33491  txpss3v  33729  fixssdm  33757  fixssrn  33758  limitssson  33762  fneer  34091  neibastop1  34097  neibastop2lem  34098  filnetlem3  34118  ontopbas  34166  bj-disj2r  34745  bj-restpw  34787  bj-discrmoore  34806  bj-idres  34855  bj-fvsnun2  34951  bj-ablssgrp  34971  bj-flddrng  34983  taupilemrplb  35014  taupilem2  35016  taupi  35017  ptrest  35336  poimirlem29  35366  mblfinlem3  35376  mblfinlem4  35377  ismblfin  35378  mbfposadd  35384  sstotbnd2  35492  ssbnd  35506  heibor1lem  35527  heiborlem1  35529  heiborlem3  35531  heiborlem5  35533  heiborlem6  35534  heiborlem10  35538  heibor  35539  opidonOLD  35570  exidcl  35594  flddivrng  35717  iss2  36041  xrnss3v  36064  refrelsredund2  36308  lshpinN  36565  lcvexchlem5  36614  pmodlem2  37423  pmod1i  37424  pmodN  37426  osumcllem7N  37538  pexmidlem4N  37549  pl42lem3N  37557  djaclN  38712  dihoml4c  38952  dochdmj1  38966  djhcl  38976  dochexmidlem4  39039  mapd1o  39224  mapdin  39238  elrfi  40008  elrfirn  40009  elrfirn2  40010  ismrcd1  40012  istopclsd  40014  isnacs2  40020  mrefg3  40022  isnacs3  40024  diophrw  40073  diophin  40086  aomclem2  40372  islmodfg  40386  lsmfgcl  40391  lmhmfgima  40401  lmhmfgsplit  40403  lmhmlnmsplit  40404  pwfi2f1o  40413  hbt  40447  harval3  40617  elinintrab  40650  trrelind  40739  clsk3nimkb  41116  isotone2  41125  onfrALTlem2  41625  onfrALTlem2VD  41968  unirestss  42132  inmap  42208  fsumiunss  42583  islptre  42627  sumnnodd  42638  limclner  42659  liminfval4  42797  liminfval3  42798  cnrefiisplem  42837  cncfuni  42894  ismbl3  42994  ismbl4  43001  fouriersw  43239  qndenserrnbllem  43302  salincl  43331  salgencntex  43349  sge0less  43397  sge0resplit  43411  sge0split  43414  sge0iunmptlemre  43420  carageniuncllem1  43526  carageniuncllem2  43527  caragenel2d  43537  hspmbllem3  43633  hspmbl  43634  ovolval2lem  43648  sssmf  43738  smfaddlem1  43762  smflimlem2  43771  smflimlem3  43772  smflimlem4  43773  smfres  43788  smfmullem4  43792  smfsuplem1  43808  rngcbas  44956  rngchomfval  44957  rngccofval  44961  dfrngc2  44963  rnghmsscmap2  44964  rnghmsscmap  44965  rngcsect  44971  funcrngcsetc  44989  ringcbas  45002  ringchomfval  45003  ringccofval  45007  dfringc2  45009  rhmsscmap2  45010  rhmsscmap  45011  rhmsscrnghm  45017  ringcsect  45022  funcringcsetc  45026  funcringcsetcALTV2lem9  45035  fldc  45074  fldhmsubc  45075  rngcrescrhm  45076  rhmsubclem1  45077  fldcALTV  45092  fldhmsubcALTV  45093  rngcrescrhmALTV  45094  rhmsubcALTVlem1  45095  setrec2fun  45613