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  27744  axtgcgrid  27745  axtgsegcon  27746  axtg5seg  27747  axtgbtwnid  27748  axtgpasch  27749  axtgcont1  27750  phnv  30098  minvecolem2  30159  minvecolem3  30160  minvecolem5  30165  minvecolem6  30166  minvecolem7  30167  hlimcaui  30520  chdmm1i  30761  chabs1  30800  chabs2  30801  ledii  30820  lejdii  30822  pjoml4i  30871  cmbr3i  30884  cmbr4i  30885  cmm1i  30890  osumcor2i  30928  3oalem4  30949  pjssmii  30965  pjocini  30982  pjini  30983  mayete3i  31012  riesz4  31348  riesz1  31349  cnlnadjeui  31361  cnlnadjeu  31362  cnlnssadj  31364  nmopadjlei  31372  pjin1i  31476  pjclem1  31479  stji1i  31526  stm1i  31527  dmdbr2  31587  ssmd1  31595  mdslj2i  31604  mdsl2bi  31607  mdslmd1lem1  31609  mdslmd2i  31614  atomli  31666  atcvat4i  31681  sumdmdlem2  31703  dmdbr5ati  31706  dmdbr6ati  31707  dmdbr7ati  31708  indifbi  31789  disjxpin  31850  imadifxp  31863  nfpconfp  31887  off2  31897  ffsrn  31985  gsummptres  32235  xrge0tsmsd  32240  idlinsubrg  32580  ordtrestNEW  32932  qqhnm  33001  qqhcn  33002  rrhre  33032  indsumin  33051  indf1ofs  33055  esumval  33075  esumel  33076  gsumesum  33088  esumlub  33089  esumcst  33092  esumfsup  33099  esumpcvgval  33107  esumcvg  33115  sigainb  33165  ldgenpisyslem1  33192  measinb2  33252  sibfinima  33369  sibfof  33370  eulerpartlemelr  33387  eulerpartlem1  33397  eulerpartgbij  33402  eulerpartlemgu  33407  eulerpartlemgs2  33410  sseqf  33422  ballotlemfelz  33520  ballotlemfp1  33521  reprinrn  33661  reprinfz1  33665  hgt750lemd  33691  bnj1292  33857  connpconn  34257  iccllysconn  34272  cvmsss2  34296  cvmcov2  34297  cvmopnlem  34300  cvmliftmolem2  34304  cvmliftlem15  34320  cvmlift2lem12  34336  mvrsfpw  34528  msrf  34564  elmsta  34570  mthmpps  34604  nepss  34718  dfon2lem4  34789  txpss3v  34881  fixssdm  34909  fixssrn  34910  limitssson  34914  gg-dvmulbr  35206  gg-dvfsumle  35213  fneer  35286  neibastop1  35292  neibastop2lem  35293  filnetlem3  35313  ontopbas  35361  bj-disj2r  35957  bj-restpw  36021  bj-discrmoore  36040  bj-idres  36089  bj-fvsnun2  36185  bj-ablssgrp  36205  bj-fldssdrng  36217  taupilemrplb  36249  taupilem2  36251  taupi  36252  ptrest  36535  poimirlem29  36565  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  mbfposadd  36583  sstotbnd2  36690  ssbnd  36704  heibor1lem  36725  heiborlem1  36727  heiborlem3  36729  heiborlem5  36731  heiborlem6  36732  heiborlem10  36736  heibor  36737  opidonOLD  36768  exidcl  36792  flddivrng  36915  iss2  37261  xrnss3v  37290  refrelsredund2  37551  lshpinN  37907  lcvexchlem5  37956  pmodlem2  38766  pmod1i  38767  pmodN  38769  osumcllem7N  38881  pexmidlem4N  38892  pl42lem3N  38900  djaclN  40055  dihoml4c  40295  dochdmj1  40309  djhcl  40319  dochexmidlem4  40382  mapd1o  40567  mapdin  40581  elrfi  41480  elrfirn  41481  elrfirn2  41482  ismrcd1  41484  istopclsd  41486  isnacs2  41492  mrefg3  41494  isnacs3  41496  diophrw  41545  diophin  41558  aomclem2  41845  islmodfg  41859  lsmfgcl  41864  lmhmfgima  41874  lmhmfgsplit  41876  lmhmlnmsplit  41877  pwfi2f1o  41886  hbt  41920  ofoafg  42152  harval3  42337  elinintrab  42376  trrelind  42464  clsk3nimkb  42839  isotone2  42848  ismnushort  43108  onfrALTlem2  43355  onfrALTlem2VD  43698  unirestss  43861  inmap  43956  fsumiunss  44339  islptre  44383  sumnnodd  44394  limclner  44415  liminfval4  44553  liminfval3  44554  cnrefiisplem  44593  cncfuni  44650  ismbl3  44750  ismbl4  44757  fouriersw  44995  qndenserrnbllem  45058  salincl  45088  salgencntex  45107  sge0less  45156  sge0resplit  45170  sge0split  45173  sge0iunmptlemre  45179  carageniuncllem1  45285  carageniuncllem2  45286  caragenel2d  45296  hspmbllem3  45392  hspmbl  45393  ovolval2lem  45407  sssmf  45502  smfaddlem1  45527  smflimlem2  45536  smflimlem3  45537  smflimlem4  45538  smfres  45554  smfmullem4  45558  smfsuplem1  45575  fcoreslem2  45822  rngcbas  46911  rngchomfval  46912  rngccofval  46916  dfrngc2  46918  rnghmsscmap2  46919  rnghmsscmap  46920  rngcsect  46926  funcrngcsetc  46944  ringcbas  46957  ringchomfval  46958  ringccofval  46962  dfringc2  46964  rhmsscmap2  46965  rhmsscmap  46966  rhmsscrnghm  46972  ringcsect  46977  funcringcsetc  46981  funcringcsetcALTV2lem9  46990  fldc  47029  fldhmsubc  47030  rngcrescrhm  47031  rhmsubclem1  47032  fldcALTV  47047  fldhmsubcALTV  47048  rngcrescrhmALTV  47049  rhmsubcALTVlem1  47050  iscnrm3llem2  47631  setrec2fun  47785