Theorem inss1 4162

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

Syntax hints:   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  inss2  4163  ssinss1  4171  unabs  4188  nssinpss  4190  dfin4  4201  inv1  4328  disjdif  4405  ifssun  4476  uniintsn  4918  wefrc  5583  relin1  5722  resss  5916  resmpt3  5946  cnvcnvss  6097  resdmss  6138  resssxp  6173  predss  6210  ordtri3or  6298  onfr  6305  ordelinel  6364  funin  6510  funimass2  6517  fnresin1  6557  fnres  6559  fresin  6643  fresaun  6645  nfvres  6810  ssimaex  6853  fneqeql2  6924  fnfvimad  7110  funiunfv  7121  isoini2  7210  ofrfvalg  7541  ofval  7544  ofrval  7545  off  7551  ofres  7552  ofco  7556  fparlem3  7954  fparlem4  7955  frrlem4  8105  frrlem13  8114  smores  8183  smores2  8185  tfrlem5  8211  pmresg  8658  sbthlem7  8876  sbthcl  8882  infi  9043  imafiALT  9112  ixpfi2  9117  unifpw  9122  elfiun  9189  dffi3  9190  marypha1lem  9192  ordtypelem6  9282  ordtypelem7  9283  ordtypelem8  9284  wdomima2g  9345  frmin  9507  frrlem15  9515  frrlem16  9516  tskwe  9708  ackbij1lem15  9990  ackbij1lem16  9991  fin23lem23  10082  fin23lem22  10083  fin23lem19  10092  brdom3  10284  brdom5  10285  brdom4  10286  imadomg  10290  fpwwe2lem11  10397  canthp1lem2  10409  wunin  10469  tskin  10515  gruima  10558  ingru  10571  gruina  10574  grur1a  10575  nqerf  10686  nqerrel  10688  hashun3  14099  hashin  14126  hashdif  14128  xptrrel  14691  rexanuz  15057  limsupgle  15186  rlimres  15267  lo1res  15268  lo1resb  15273  rlimresb  15274  o1resb  15275  lo1eq  15277  rlimeq  15278  o1of2  15322  o1rlimmul  15328  isercolllem2  15377  isercolllem3  15378  isercoll  15379  incexclem  15548  incexc  15549  bitsinvp1  16156  sadcaddlem  16164  sadadd2lem  16166  sadadd3  16168  sadaddlem  16173  sadasslem  16177  sadeq  16179  bitsres  16180  smuval2  16189  smupval  16195  smueqlem  16197  smumul  16200  ramub2  16715  ramub1lem2  16728  fvsetsid  16869  ressinbas  16955  ressress  16958  submre  17314  isacs1i  17366  mreacs  17367  acsfn  17368  invss  17473  sscres  17535  catcisolem  17825  catciso  17826  isacs5lem  18263  psss  18298  tsrss  18307  tsrdir  18322  sylow2a  19224  lsmmod  19281  gsumzres  19510  gsumzaddlem  19522  dprddisj2  19642  ablfac1eu  19676  isunit  19899  acsfn1p  20067  lspextmo  20318  2idlval  20504  pjfval  20913  pjpm  20915  aspsubrg  21080  psrbagsn  21271  ofco2  21600  basdif0  22103  tgval2  22106  eltg3  22112  tgcl  22119  tgdom  22128  tgidm  22130  ppttop  22157  epttop  22159  ntropn  22200  ntrin  22212  mretopd  22243  neiptoptop  22282  restfpw  22330  neitr  22331  restcls  22332  cncls  22425  cnpresti  22439  cnprest  22440  cmpsublem  22550  cmpsub  22551  fiuncmp  22555  indisconn  22569  connsub  22572  iunconnlem  22578  islly2  22635  cldllycmp  22646  kgentopon  22689  ptbasfi  22732  ptcnplem  22772  txcnmpt  22775  txcmplem2  22793  hausdiag  22796  txkgen  22803  xkococnlem  22810  qtoptop2  22850  basqtop  22862  fbssfi  22988  filin  23005  infil  23014  fbasrn  23035  fgtr  23041  ufprim  23060  flimrest  23134  txflf  23157  fclsrest  23175  alexsubALTlem4  23201  tsmsres  23295  tsmsxplem1  23304  ustund  23373  trust  23381  utoptop  23386  restutop  23389  cfiluweak  23447  xmetres  23517  metres  23518  blin2  23582  setsmstopn  23633  metrest  23680  ressxms  23681  tgioo  23959  xrsmopn  23975  reconnlem1  23989  xrge0tsms  23997  tcphcph  24401  cfilresi  24459  cfilres  24460  caussi  24461  causs  24462  relcmpcmet  24482  minveclem4a  24594  ismbl2  24691  cmmbl  24698  nulmbl2  24700  unmbl  24701  shftmbl  24702  volinun  24710  voliunlem1  24714  voliunlem2  24715  ioombl1lem4  24725  ioombl1  24726  uniioombllem2  24747  uniioombllem3  24749  uniioombllem4  24750  uniioombllem5  24751  uniioombl  24753  volivth  24771  vitalilem3  24774  vitalilem4  24775  vitalilem5  24776  vitali  24777  mbfadd  24825  mbfsub  24826  i1fadd  24859  itg1addlem2  24861  itg1addlem4  24863  itg1addlem4OLD  24864  itg1addlem5  24865  itg1climres  24879  mbfmul  24891  itg2splitlem  24913  itg2split  24914  limcresi  25049  limciun  25058  dvreslem  25073  dvres2lem  25074  dvres  25075  dvres3a  25078  dvaddbr  25102  dvmulbr  25103  dvfsumle  25185  dvfsumabs  25187  ig1peu  25336  pilem2  25611  pilem3  25612  rlimcnp2  26116  ppisval  26253  ppifi  26255  ppiprm  26300  chtprm  26302  chtdif  26307  efchtdvds  26308  ppidif  26312  ppiltx  26326  prmorcht  26327  ppiub  26352  chtlepsi  26354  pclogsum  26363  vmasum  26364  chpval2  26366  chpub  26368  2sqlem8  26574  chebbnd1lem1  26617  chtppilimlem1  26621  rpvmasum2  26660  dchrisum0re  26661  rplogsum  26675  dirith2  26676  axtgcgrrflx  26823  axtgcgrid  26824  axtgsegcon  26825  axtg5seg  26826  axtgbtwnid  26827  axtgpasch  26828  axtgcont1  26829  phnv  29176  minvecolem2  29237  minvecolem3  29238  minvecolem5  29243  minvecolem6  29244  minvecolem7  29245  hlimcaui  29598  chdmm1i  29839  chabs1  29878  chabs2  29879  ledii  29898  lejdii  29900  pjoml4i  29949  cmbr3i  29962  cmbr4i  29963  cmm1i  29968  osumcor2i  30006  3oalem4  30027  pjssmii  30043  pjocini  30060  pjini  30061  mayete3i  30090  riesz4  30426  riesz1  30427  cnlnadjeui  30439  cnlnadjeu  30440  cnlnssadj  30442  nmopadjlei  30450  pjin1i  30554  pjclem1  30557  stji1i  30604  stm1i  30605  dmdbr2  30665  ssmd1  30673  mdslj2i  30682  mdsl2bi  30685  mdslmd1lem1  30687  mdslmd2i  30692  atomli  30744  atcvat4i  30759  sumdmdlem2  30781  dmdbr5ati  30784  dmdbr6ati  30785  dmdbr7ati  30786  indifbi  30868  disjxpin  30927  imadifxp  30940  nfpconfp  30967  off2  30978  ffsrn  31064  gsummptres  31312  xrge0tsmsd  31317  idlinsubrg  31608  ordtrestNEW  31871  qqhnm  31940  qqhcn  31941  rrhre  31971  indsumin  31990  indf1ofs  31994  esumval  32014  esumel  32015  gsumesum  32027  esumlub  32028  esumcst  32031  esumfsup  32038  esumpcvgval  32046  esumcvg  32054  sigainb  32104  ldgenpisyslem1  32131  measinb2  32191  sibfinima  32306  sibfof  32307  eulerpartlemelr  32324  eulerpartlem1  32334  eulerpartgbij  32339  eulerpartlemgu  32344  eulerpartlemgs2  32347  sseqf  32359  ballotlemfelz  32457  ballotlemfp1  32458  reprinrn  32598  reprinfz1  32602  hgt750lemd  32628  bnj1292  32795  connpconn  33197  iccllysconn  33212  cvmsss2  33236  cvmcov2  33237  cvmopnlem  33240  cvmliftmolem2  33244  cvmliftlem15  33260  cvmlift2lem12  33276  mvrsfpw  33468  msrf  33504  elmsta  33510  mthmpps  33544  nepss  33662  dfon2lem4  33762  nosupbnd1lem1  33911  nosupbnd2  33919  noinfbnd1lem1  33926  txpss3v  34180  fixssdm  34208  fixssrn  34209  limitssson  34213  fneer  34542  neibastop1  34548  neibastop2lem  34549  filnetlem3  34569  ontopbas  34617  bj-disj2r  35218  bj-restpw  35263  bj-discrmoore  35282  bj-idres  35331  bj-fvsnun2  35427  bj-ablssgrp  35447  bj-fldssdrng  35459  taupilemrplb  35491  taupilem2  35493  taupi  35494  ptrest  35776  poimirlem29  35806  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  mbfposadd  35824  sstotbnd2  35932  ssbnd  35946  heibor1lem  35967  heiborlem1  35969  heiborlem3  35971  heiborlem5  35973  heiborlem6  35974  heiborlem10  35978  heibor  35979  opidonOLD  36010  exidcl  36034  flddivrng  36157  iss2  36479  xrnss3v  36502  refrelsredund2  36746  lshpinN  37003  lcvexchlem5  37052  pmodlem2  37861  pmod1i  37862  pmodN  37864  osumcllem7N  37976  pexmidlem4N  37987  pl42lem3N  37995  djaclN  39150  dihoml4c  39390  dochdmj1  39404  djhcl  39414  dochexmidlem4  39477  mapd1o  39662  mapdin  39676  elrfi  40516  elrfirn  40517  elrfirn2  40518  ismrcd1  40520  istopclsd  40522  isnacs2  40528  mrefg3  40530  isnacs3  40532  diophrw  40581  diophin  40594  aomclem2  40880  islmodfg  40894  lsmfgcl  40899  lmhmfgima  40909  lmhmfgsplit  40911  lmhmlnmsplit  40912  pwfi2f1o  40921  hbt  40955  harval3  41145  elinintrab  41185  trrelind  41273  clsk3nimkb  41650  isotone2  41659  ismnushort  41919  onfrALTlem2  42166  onfrALTlem2VD  42509  unirestss  42673  inmap  42749  fsumiunss  43116  islptre  43160  sumnnodd  43171  limclner  43192  liminfval4  43330  liminfval3  43331  cnrefiisplem  43370  cncfuni  43427  ismbl3  43527  ismbl4  43534  fouriersw  43772  qndenserrnbllem  43835  salincl  43864  salgencntex  43882  sge0less  43930  sge0resplit  43944  sge0split  43947  sge0iunmptlemre  43953  carageniuncllem1  44059  carageniuncllem2  44060  caragenel2d  44070  hspmbllem3  44166  hspmbl  44167  ovolval2lem  44181  sssmf  44274  smfaddlem1  44298  smflimlem2  44307  smflimlem3  44308  smflimlem4  44309  smfres  44324  smfmullem4  44328  smfsuplem1  44344  fcoreslem2  44558  rngcbas  45523  rngchomfval  45524  rngccofval  45528  dfrngc2  45530  rnghmsscmap2  45531  rnghmsscmap  45532  rngcsect  45538  funcrngcsetc  45556  ringcbas  45569  ringchomfval  45570  ringccofval  45574  dfringc2  45576  rhmsscmap2  45577  rhmsscmap  45578  rhmsscrnghm  45584  ringcsect  45589  funcringcsetc  45593  funcringcsetcALTV2lem9  45602  fldc  45641  fldhmsubc  45642  rngcrescrhm  45643  rhmsubclem1  45644  fldcALTV  45659  fldhmsubcALTV  45660  rngcrescrhmALTV  45661  rhmsubcALTVlem1  45662  iscnrm3llem2  46244  setrec2fun  46398