Theorem inss1 4229

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

Syntax hints:   ∩ cin 3948   ⊆ wss 3949

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  inss2  4230  ssinss1  4238  unabs  4255  nssinpss  4257  dfin4  4268  inv1  4395  disjdif  4472  ifssun  4546  uniintsn  4992  wefrc  5671  relin1  5813  resss  6007  resmpt3  6039  cnvcnvss  6194  resdmss  6235  resssxp  6270  predss  6309  ordtri3or  6397  onfr  6404  ordelinel  6466  funin  6625  funimass2  6632  fnresin1  6676  fnres  6678  fresin  6761  fresaun  6763  nfvres  6933  ssimaex  6977  fneqeql2  7049  fnfvimad  7236  funiunfv  7247  isoini2  7336  ofrfvalg  7678  ofval  7681  ofrval  7682  off  7688  ofres  7689  ofco  7693  fparlem3  8100  fparlem4  8101  frrlem4  8274  frrlem13  8283  smores  8352  smores2  8354  tfrlem5  8380  pmresg  8864  sbthlem7  9089  sbthcl  9095  infi  9268  imafiALT  9345  ixpfi2  9350  unifpw  9355  elfiun  9425  dffi3  9426  marypha1lem  9428  ordtypelem6  9518  ordtypelem7  9519  ordtypelem8  9520  wdomima2g  9581  frmin  9744  frrlem15  9752  frrlem16  9753  tskwe  9945  ackbij1lem15  10229  ackbij1lem16  10230  fin23lem23  10321  fin23lem22  10322  fin23lem19  10331  brdom3  10523  brdom5  10524  brdom4  10525  imadomg  10529  fpwwe2lem11  10636  canthp1lem2  10648  wunin  10708  tskin  10754  gruima  10797  ingru  10810  gruina  10813  grur1a  10814  nqerf  10925  nqerrel  10927  hashun3  14344  hashin  14371  hashdif  14373  xptrrel  14927  rexanuz  15292  limsupgle  15421  rlimres  15502  lo1res  15503  lo1resb  15508  rlimresb  15509  o1resb  15510  lo1eq  15512  rlimeq  15513  o1of2  15557  o1rlimmul  15563  isercolllem2  15612  isercolllem3  15613  isercoll  15614  incexclem  15782  incexc  15783  bitsinvp1  16390  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  sadasslem  16411  sadeq  16413  bitsres  16414  smuval2  16423  smupval  16429  smueqlem  16431  smumul  16434  ramub2  16947  ramub1lem2  16960  fvsetsid  17101  ressbasss2  17185  ressinbas  17190  ressress  17193  submre  17549  isacs1i  17601  mreacs  17602  acsfn  17603  invss  17708  sscres  17770  catcisolem  18060  catciso  18061  isacs5lem  18498  psss  18533  tsrss  18542  tsrdir  18557  sylow2a  19487  lsmmod  19543  gsumzres  19777  gsumzaddlem  19789  dprddisj2  19909  ablfac1eu  19943  isunit  20187  acsfn1p  20415  lspextmo  20667  2idlval  20858  pjfval  21261  pjpm  21263  aspsubrg  21430  psrbagsn  21624  ofco2  21953  basdif0  22456  tgval2  22459  eltg3  22465  tgcl  22472  tgdom  22481  tgidm  22483  ppttop  22510  epttop  22512  ntropn  22553  ntrin  22565  mretopd  22596  neiptoptop  22635  restfpw  22683  neitr  22684  restcls  22685  cncls  22778  cnpresti  22792  cnprest  22793  cmpsublem  22903  cmpsub  22904  fiuncmp  22908  indisconn  22922  connsub  22925  iunconnlem  22931  islly2  22988  cldllycmp  22999  kgentopon  23042  ptbasfi  23085  ptcnplem  23125  txcnmpt  23128  txcmplem2  23146  hausdiag  23149  txkgen  23156  xkococnlem  23163  qtoptop2  23203  basqtop  23215  fbssfi  23341  filin  23358  infil  23367  fbasrn  23388  fgtr  23394  ufprim  23413  flimrest  23487  txflf  23510  fclsrest  23528  alexsubALTlem4  23554  tsmsres  23648  tsmsxplem1  23657  ustund  23726  trust  23734  utoptop  23739  restutop  23742  cfiluweak  23800  xmetres  23870  metres  23871  blin2  23935  setsmstopn  23986  metrest  24033  ressxms  24034  tgioo  24312  xrsmopn  24328  reconnlem1  24342  xrge0tsms  24350  tcphcph  24754  cfilresi  24812  cfilres  24813  caussi  24814  causs  24815  relcmpcmet  24835  minveclem4a  24947  ismbl2  25044  cmmbl  25051  nulmbl2  25053  unmbl  25054  shftmbl  25055  volinun  25063  voliunlem1  25067  voliunlem2  25068  ioombl1lem4  25078  ioombl1  25079  uniioombllem2  25100  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombl  25106  volivth  25124  vitalilem3  25127  vitalilem4  25128  vitalilem5  25129  vitali  25130  mbfadd  25178  mbfsub  25179  i1fadd  25212  itg1addlem2  25214  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  itg1climres  25232  mbfmul  25244  itg2splitlem  25266  itg2split  25267  limcresi  25402  limciun  25411  dvreslem  25426  dvres2lem  25427  dvres  25428  dvres3a  25431  dvaddbr  25455  dvmulbr  25456  dvfsumle  25538  dvfsumabs  25540  ig1peu  25689  pilem2  25964  pilem3  25965  rlimcnp2  26471  ppisval  26608  ppifi  26610  ppiprm  26655  chtprm  26657  chtdif  26662  efchtdvds  26663  ppidif  26667  ppiltx  26681  prmorcht  26682  ppiub  26707  chtlepsi  26709  pclogsum  26718  vmasum  26719  chpval2  26721  chpub  26723  2sqlem8  26929  chebbnd1lem1  26972  chtppilimlem1  26976  rpvmasum2  27015  dchrisum0re  27016  rplogsum  27030  dirith2  27031  nosupbnd1lem1  27211  nosupbnd2  27219  noinfbnd1lem1  27226  axtgcgrrflx  27713  axtgcgrid  27714  axtgsegcon  27715  axtg5seg  27716  axtgbtwnid  27717  axtgpasch  27718  axtgcont1  27719  phnv  30067  minvecolem2  30128  minvecolem3  30129  minvecolem5  30134  minvecolem6  30135  minvecolem7  30136  hlimcaui  30489  chdmm1i  30730  chabs1  30769  chabs2  30770  ledii  30789  lejdii  30791  pjoml4i  30840  cmbr3i  30853  cmbr4i  30854  cmm1i  30859  osumcor2i  30897  3oalem4  30918  pjssmii  30934  pjocini  30951  pjini  30952  mayete3i  30981  riesz4  31317  riesz1  31318  cnlnadjeui  31330  cnlnadjeu  31331  cnlnssadj  31333  nmopadjlei  31341  pjin1i  31445  pjclem1  31448  stji1i  31495  stm1i  31496  dmdbr2  31556  ssmd1  31564  mdslj2i  31573  mdsl2bi  31576  mdslmd1lem1  31578  mdslmd2i  31583  atomli  31635  atcvat4i  31650  sumdmdlem2  31672  dmdbr5ati  31675  dmdbr6ati  31676  dmdbr7ati  31677  indifbi  31758  disjxpin  31819  imadifxp  31832  nfpconfp  31856  off2  31866  ffsrn  31954  gsummptres  32204  xrge0tsmsd  32209  idlinsubrg  32549  ordtrestNEW  32901  qqhnm  32970  qqhcn  32971  rrhre  33001  indsumin  33020  indf1ofs  33024  esumval  33044  esumel  33045  gsumesum  33057  esumlub  33058  esumcst  33061  esumfsup  33068  esumpcvgval  33076  esumcvg  33084  sigainb  33134  ldgenpisyslem1  33161  measinb2  33221  sibfinima  33338  sibfof  33339  eulerpartlemelr  33356  eulerpartlem1  33366  eulerpartgbij  33371  eulerpartlemgu  33376  eulerpartlemgs2  33379  sseqf  33391  ballotlemfelz  33489  ballotlemfp1  33490  reprinrn  33630  reprinfz1  33634  hgt750lemd  33660  bnj1292  33826  connpconn  34226  iccllysconn  34241  cvmsss2  34265  cvmcov2  34266  cvmopnlem  34269  cvmliftmolem2  34273  cvmliftlem15  34289  cvmlift2lem12  34305  mvrsfpw  34497  msrf  34533  elmsta  34539  mthmpps  34573  nepss  34687  dfon2lem4  34758  txpss3v  34850  fixssdm  34878  fixssrn  34879  limitssson  34883  gg-dvmulbr  35175  gg-dvfsumle  35182  fneer  35238  neibastop1  35244  neibastop2lem  35245  filnetlem3  35265  ontopbas  35313  bj-disj2r  35909  bj-restpw  35973  bj-discrmoore  35992  bj-idres  36041  bj-fvsnun2  36137  bj-ablssgrp  36157  bj-fldssdrng  36169  taupilemrplb  36201  taupilem2  36203  taupi  36204  ptrest  36487  poimirlem29  36517  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  mbfposadd  36535  sstotbnd2  36642  ssbnd  36656  heibor1lem  36677  heiborlem1  36679  heiborlem3  36681  heiborlem5  36683  heiborlem6  36684  heiborlem10  36688  heibor  36689  opidonOLD  36720  exidcl  36744  flddivrng  36867  iss2  37213  xrnss3v  37242  refrelsredund2  37503  lshpinN  37859  lcvexchlem5  37908  pmodlem2  38718  pmod1i  38719  pmodN  38721  osumcllem7N  38833  pexmidlem4N  38844  pl42lem3N  38852  djaclN  40007  dihoml4c  40247  dochdmj1  40261  djhcl  40271  dochexmidlem4  40334  mapd1o  40519  mapdin  40533  elrfi  41432  elrfirn  41433  elrfirn2  41434  ismrcd1  41436  istopclsd  41438  isnacs2  41444  mrefg3  41446  isnacs3  41448  diophrw  41497  diophin  41510  aomclem2  41797  islmodfg  41811  lsmfgcl  41816  lmhmfgima  41826  lmhmfgsplit  41828  lmhmlnmsplit  41829  pwfi2f1o  41838  hbt  41872  ofoafg  42104  harval3  42289  elinintrab  42328  trrelind  42416  clsk3nimkb  42791  isotone2  42800  ismnushort  43060  onfrALTlem2  43307  onfrALTlem2VD  43650  unirestss  43813  inmap  43908  fsumiunss  44291  islptre  44335  sumnnodd  44346  limclner  44367  liminfval4  44505  liminfval3  44506  cnrefiisplem  44545  cncfuni  44602  ismbl3  44702  ismbl4  44709  fouriersw  44947  qndenserrnbllem  45010  salincl  45040  salgencntex  45059  sge0less  45108  sge0resplit  45122  sge0split  45125  sge0iunmptlemre  45131  carageniuncllem1  45237  carageniuncllem2  45238  caragenel2d  45248  hspmbllem3  45344  hspmbl  45345  ovolval2lem  45359  sssmf  45454  smfaddlem1  45479  smflimlem2  45488  smflimlem3  45489  smflimlem4  45490  smfres  45506  smfmullem4  45510  smfsuplem1  45527  fcoreslem2  45774  rngcbas  46863  rngchomfval  46864  rngccofval  46868  dfrngc2  46870  rnghmsscmap2  46871  rnghmsscmap  46872  rngcsect  46878  funcrngcsetc  46896  ringcbas  46909  ringchomfval  46910  ringccofval  46914  dfringc2  46916  rhmsscmap2  46917  rhmsscmap  46918  rhmsscrnghm  46924  ringcsect  46929  funcringcsetc  46933  funcringcsetcALTV2lem9  46942  fldc  46981  fldhmsubc  46982  rngcrescrhm  46983  rhmsubclem1  46984  fldcALTV  46999  fldhmsubcALTV  47000  rngcrescrhmALTV  47001  rhmsubcALTVlem1  47002  iscnrm3llem2  47583  setrec2fun  47737