Theorem inss1 4187

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

Syntax hints:   ∩ cin 3898   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-ss 3916

This theorem is referenced by:  inss2  4188  ssinss1  4196  unabs  4215  nssinpss  4217  dfin4  4228  inv1  4348  disjdif  4422  ifssun  4495  uniintsn  4938  wefrc  5616  relin1  5759  resss  5958  resmpt3  5995  cnvcnvss  6150  resdmss  6191  resssxp  6226  predss  6265  ordtri3or  6347  onfr  6354  ordelinel  6418  funin  6566  funimass2  6573  fnresin1  6615  fnres  6617  fresin  6701  fresaun  6703  nfvres  6870  ssimaex  6917  fneqeql2  6990  fnfvimad  7178  funiunfv  7192  isoini2  7283  ofrfvalg  7628  ofval  7631  ofrval  7632  off  7638  ofres  7639  ofco  7645  fparlem3  8054  fparlem4  8055  frrlem4  8229  frrlem13  8238  smores  8282  smores2  8284  tfrlem5  8309  pmresg  8806  sbthlem7  9019  sbthcl  9025  infi  9168  imafi  9213  ixpfi2  9248  unifpw  9253  elfiun  9331  dffi3  9332  marypha1lem  9334  ordtypelem6  9426  ordtypelem7  9427  ordtypelem8  9428  wdomima2g  9489  frmin  9659  frrlem15  9667  frrlem16  9668  tskwe  9860  ackbij1lem15  10141  ackbij1lem16  10142  fin23lem23  10234  fin23lem22  10235  fin23lem19  10244  brdom3  10436  brdom5  10437  brdom4  10438  imadomg  10442  fpwwe2lem11  10550  canthp1lem2  10562  wunin  10622  tskin  10668  gruima  10711  ingru  10724  gruina  10727  grur1a  10728  nqerf  10839  nqerrel  10841  hashun3  14305  hashin  14332  hashdif  14334  xptrrel  14901  rexanuz  15267  limsupgle  15398  rlimres  15479  lo1res  15480  lo1resb  15485  rlimresb  15486  o1resb  15487  lo1eq  15489  rlimeq  15490  o1of2  15534  o1rlimmul  15540  isercolllem2  15587  isercolllem3  15588  isercoll  15589  incexclem  15757  incexc  15758  bitsinvp1  16374  sadcaddlem  16382  sadadd2lem  16384  sadadd3  16386  sadaddlem  16391  sadasslem  16395  sadeq  16397  bitsres  16398  smuval2  16407  smupval  16413  smueqlem  16415  smumul  16418  ramub2  16940  ramub1lem2  16953  fvsetsid  17093  ressbasss2  17166  ressinbas  17170  ressress  17172  submre  17522  isacs1i  17578  mreacs  17579  acsfn  17580  invss  17683  sscres  17745  catcisolem  18032  catciso  18033  isacs5lem  18466  psss  18501  tsrss  18510  tsrdir  18525  sylow2a  19546  lsmmod  19602  gsumzres  19836  gsumzaddlem  19848  dprddisj2  19968  ablfac1eu  20002  isunit  20307  rngcbas  20552  rngchomfval  20553  rngccofval  20557  dfrngc2  20559  rnghmsscmap2  20560  rnghmsscmap  20561  rngcsect  20567  funcrngcsetc  20571  ringcbas  20581  ringchomfval  20582  ringccofval  20586  dfringc2  20588  rhmsscmap2  20589  rhmsscmap  20590  rhmsscrnghm  20596  ringcsect  20601  funcringcsetc  20605  rngcrescrhm  20615  rhmsubclem1  20616  fldc  20715  fldhmsubc  20716  acsfn1p  20730  lspextmo  21006  2idlval  21204  pjfval  21659  pjpm  21661  aspsubrg  21829  psrbagsn  22016  ofco2  22393  basdif0  22895  tgval2  22898  eltg3  22904  tgcl  22911  tgdom  22920  tgidm  22922  ppttop  22949  epttop  22951  ntropn  22991  ntrin  23003  mretopd  23034  neiptoptop  23073  restfpw  23121  neitr  23122  restcls  23123  cncls  23216  cnpresti  23230  cnprest  23231  cmpsublem  23341  cmpsub  23342  fiuncmp  23346  indisconn  23360  connsub  23363  iunconnlem  23369  islly2  23426  cldllycmp  23437  kgentopon  23480  ptbasfi  23523  ptcnplem  23563  txcnmpt  23566  txcmplem2  23584  hausdiag  23587  txkgen  23594  xkococnlem  23601  qtoptop2  23641  basqtop  23653  fbssfi  23779  filin  23796  infil  23805  fbasrn  23826  fgtr  23832  ufprim  23851  flimrest  23925  txflf  23948  fclsrest  23966  alexsubALTlem4  23992  tsmsres  24086  tsmsxplem1  24095  ustund  24164  trust  24171  utoptop  24176  restutop  24179  cfiluweak  24236  xmetres  24306  metres  24307  blin2  24371  setsmstopn  24420  metrest  24466  ressxms  24467  tgioo  24738  xrsmopn  24755  reconnlem1  24769  xrge0tsms  24777  tcphcph  25191  cfilresi  25249  cfilres  25250  caussi  25251  causs  25252  relcmpcmet  25272  minveclem4a  25384  ismbl2  25482  cmmbl  25489  nulmbl2  25491  unmbl  25492  shftmbl  25493  volinun  25501  voliunlem1  25505  voliunlem2  25506  ioombl1lem4  25516  ioombl1  25517  uniioombllem2  25538  uniioombllem3  25540  uniioombllem4  25541  uniioombllem5  25542  uniioombl  25544  volivth  25562  vitalilem3  25565  vitalilem4  25566  vitalilem5  25567  vitali  25568  mbfadd  25616  mbfsub  25617  i1fadd  25650  itg1addlem2  25652  itg1addlem4  25654  itg1addlem5  25655  itg1climres  25669  mbfmul  25681  itg2splitlem  25703  itg2split  25704  limcresi  25840  limciun  25849  dvreslem  25864  dvres2lem  25865  dvres  25866  dvres3a  25869  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  ig1peu  26134  pilem2  26416  pilem3  26417  rlimcnp2  26930  ppisval  27068  ppifi  27070  ppiprm  27115  chtprm  27117  chtdif  27122  efchtdvds  27123  ppidif  27127  ppiltx  27141  prmorcht  27142  ppiub  27169  chtlepsi  27171  pclogsum  27180  vmasum  27181  chpval2  27183  chpub  27185  2sqlem8  27391  chebbnd1lem1  27434  chtppilimlem1  27438  rpvmasum2  27477  dchrisum0re  27478  rplogsum  27492  dirith2  27493  nosupbnd1lem1  27674  nosupbnd2  27682  noinfbnd1lem1  27689  axtgcgrrflx  28483  axtgcgrid  28484  axtgsegcon  28485  axtg5seg  28486  axtgbtwnid  28487  axtgpasch  28488  axtgcont1  28489  phnv  30838  minvecolem2  30899  minvecolem3  30900  minvecolem5  30905  minvecolem6  30906  minvecolem7  30907  hlimcaui  31260  chdmm1i  31501  chabs1  31540  chabs2  31541  ledii  31560  lejdii  31562  pjoml4i  31611  cmbr3i  31624  cmbr4i  31625  cmm1i  31630  osumcor2i  31668  3oalem4  31689  pjssmii  31705  pjocini  31722  pjini  31723  mayete3i  31752  riesz4  32088  riesz1  32089  cnlnadjeui  32101  cnlnadjeu  32102  cnlnssadj  32104  nmopadjlei  32112  pjin1i  32216  pjclem1  32219  stji1i  32266  stm1i  32267  dmdbr2  32327  ssmd1  32335  mdslj2i  32344  mdsl2bi  32347  mdslmd1lem1  32349  mdslmd2i  32354  atomli  32406  atcvat4i  32421  sumdmdlem2  32443  dmdbr5ati  32446  dmdbr6ati  32447  dmdbr7ati  32448  indifbi  32544  disjxpin  32612  imadifxp  32625  nfpconfp  32659  off2  32668  ffsrn  32756  indsumin  32892  indf1ofs  32897  gsummptres  33084  xrge0tsmsd  33104  idlinsubrg  33461  ordtrestNEW  34027  qqhnm  34096  qqhcn  34097  rrhre  34127  esumval  34152  esumel  34153  gsumesum  34165  esumlub  34166  esumcst  34169  esumfsup  34176  esumpcvgval  34184  esumcvg  34192  sigainb  34242  ldgenpisyslem1  34269  measinb2  34329  sibfinima  34445  sibfof  34446  eulerpartlemelr  34463  eulerpartlem1  34473  eulerpartgbij  34478  eulerpartlemgu  34483  eulerpartlemgs2  34486  sseqf  34498  ballotlemfelz  34597  ballotlemfp1  34598  reprinrn  34724  reprinfz1  34728  hgt750lemd  34754  bnj1292  34920  connpconn  35378  iccllysconn  35393  cvmsss2  35417  cvmcov2  35418  cvmopnlem  35421  cvmliftmolem2  35425  cvmliftlem15  35441  cvmlift2lem12  35457  mvrsfpw  35649  msrf  35685  elmsta  35691  mthmpps  35725  nepss  35861  dfon2lem4  35927  txpss3v  36019  fixssdm  36047  fixssrn  36048  limitssson  36052  fneer  36496  neibastop1  36502  neibastop2lem  36503  filnetlem3  36523  ontopbas  36571  bj-disj2r  37172  bj-restpw  37236  bj-discrmoore  37255  bj-idres  37304  bj-fvsnun2  37400  bj-ablssgrp  37420  bj-fldssdrng  37432  taupilemrplb  37464  taupilem2  37466  taupi  37467  ptrest  37759  poimirlem29  37789  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  mbfposadd  37807  sstotbnd2  37914  ssbnd  37928  heibor1lem  37949  heiborlem1  37951  heiborlem3  37953  heiborlem5  37955  heiborlem6  37956  heiborlem10  37960  heibor  37961  opidonOLD  37992  exidcl  38016  flddivrng  38139  iss2  38476  xrnss3v  38505  refrelsredund2  38829  lshpinN  39188  lcvexchlem5  39237  pmodlem2  40046  pmod1i  40047  pmodN  40049  osumcllem7N  40161  pexmidlem4N  40172  pl42lem3N  40180  djaclN  41335  dihoml4c  41575  dochdmj1  41589  djhcl  41599  dochexmidlem4  41662  mapd1o  41847  mapdin  41861  unitscyglem5  42392  redvmptabs  42557  elrfi  42878  elrfirn  42879  elrfirn2  42880  ismrcd1  42882  istopclsd  42884  isnacs2  42890  mrefg3  42892  isnacs3  42894  diophrw  42943  diophin  42956  aomclem2  43239  islmodfg  43253  lsmfgcl  43258  lmhmfgima  43268  lmhmfgsplit  43270  lmhmlnmsplit  43271  pwfi2f1o  43280  hbt  43314  ofoafg  43538  harval3  43721  elinintrab  43760  trrelind  43848  clsk3nimkb  44223  isotone2  44232  ismnushort  44484  onfrALTlem2  44729  onfrALTlem2VD  45071  wfac8prim  45185  unirestss  45310  inmap  45395  fsumiunss  45763  islptre  45807  sumnnodd  45818  limclner  45837  liminfval4  45975  liminfval3  45976  cnrefiisplem  46015  cncfuni  46072  ismbl3  46172  ismbl4  46179  fouriersw  46417  qndenserrnbllem  46480  salincl  46510  salgencntex  46529  sge0less  46578  sge0resplit  46592  sge0split  46595  sge0iunmptlemre  46601  carageniuncllem1  46707  carageniuncllem2  46708  caragenel2d  46718  hspmbllem3  46814  hspmbl  46815  ovolval2lem  46829  sssmf  46924  smfaddlem1  46949  smflimlem2  46958  smflimlem3  46959  smflimlem4  46960  smfres  46976  smfmullem4  46980  smfsuplem1  46997  fcoreslem2  47252  rngcrescrhmALTV  48468  rhmsubcALTVlem1  48469  funcringcsetcALTV2lem9  48486  fldcALTV  48520  fldhmsubcALTV  48521  iscnrm3llem2  49137  uptrlem1  49397  uptrlem2  49398  uptrlem3  49399  uptra  49402  uptrar  49403  uobeqw  49406  uptr2  49408  uptr2a  49409  fucoppcfunc  49599  setrec2fun  49879