Theorem inss1 4191

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

Syntax hints:   ∩ cin 3902   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  inss2  4192  ssinss1  4200  unabs  4219  nssinpss  4221  dfin4  4232  inv1  4352  disjdif  4426  ifssun  4499  uniintsn  4942  wefrc  5626  relin1  5769  resss  5968  resmpt3  6005  cnvcnvss  6160  resdmss  6201  resssxp  6236  predss  6275  ordtri3or  6357  onfr  6364  ordelinel  6428  funin  6576  funimass2  6583  fnresin1  6625  fnres  6627  fresin  6711  fresaun  6713  nfvres  6880  ssimaex  6927  fneqeql2  7001  fnfvimad  7190  funiunfv  7204  isoini2  7295  ofrfvalg  7640  ofval  7643  ofrval  7644  off  7650  ofres  7651  ofco  7657  fparlem3  8066  fparlem4  8067  frrlem4  8241  frrlem13  8250  smores  8294  smores2  8296  tfrlem5  8321  pmresg  8820  sbthlem7  9033  sbthcl  9039  infi  9182  imafi  9227  ixpfi2  9262  unifpw  9267  elfiun  9345  dffi3  9346  marypha1lem  9348  ordtypelem6  9440  ordtypelem7  9441  ordtypelem8  9442  wdomima2g  9503  frmin  9673  frrlem15  9681  frrlem16  9682  tskwe  9874  ackbij1lem15  10155  ackbij1lem16  10156  fin23lem23  10248  fin23lem22  10249  fin23lem19  10258  brdom3  10450  brdom5  10451  brdom4  10452  imadomg  10456  fpwwe2lem11  10564  canthp1lem2  10576  wunin  10636  tskin  10682  gruima  10725  ingru  10738  gruina  10741  grur1a  10742  nqerf  10853  nqerrel  10855  hashun3  14319  hashin  14346  hashdif  14348  xptrrel  14915  rexanuz  15281  limsupgle  15412  rlimres  15493  lo1res  15494  lo1resb  15499  rlimresb  15500  o1resb  15501  lo1eq  15503  rlimeq  15504  o1of2  15548  o1rlimmul  15554  isercolllem2  15601  isercolllem3  15602  isercoll  15603  incexclem  15771  incexc  15772  bitsinvp1  16388  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  sadeq  16411  bitsres  16412  smuval2  16421  smupval  16427  smueqlem  16429  smumul  16432  ramub2  16954  ramub1lem2  16967  fvsetsid  17107  ressbasss2  17180  ressinbas  17184  ressress  17186  submre  17536  isacs1i  17592  mreacs  17593  acsfn  17594  invss  17697  sscres  17759  catcisolem  18046  catciso  18047  isacs5lem  18480  psss  18515  tsrss  18524  tsrdir  18539  sylow2a  19560  lsmmod  19616  gsumzres  19850  gsumzaddlem  19862  dprddisj2  19982  ablfac1eu  20016  isunit  20321  rngcbas  20566  rngchomfval  20567  rngccofval  20571  dfrngc2  20573  rnghmsscmap2  20574  rnghmsscmap  20575  rngcsect  20581  funcrngcsetc  20585  ringcbas  20595  ringchomfval  20596  ringccofval  20600  dfringc2  20602  rhmsscmap2  20603  rhmsscmap  20604  rhmsscrnghm  20610  ringcsect  20615  funcringcsetc  20619  rngcrescrhm  20629  rhmsubclem1  20630  fldc  20729  fldhmsubc  20730  acsfn1p  20744  lspextmo  21020  2idlval  21218  pjfval  21673  pjpm  21675  aspsubrg  21843  psrbagsn  22030  ofco2  22407  basdif0  22909  tgval2  22912  eltg3  22918  tgcl  22925  tgdom  22934  tgidm  22936  ppttop  22963  epttop  22965  ntropn  23005  ntrin  23017  mretopd  23048  neiptoptop  23087  restfpw  23135  neitr  23136  restcls  23137  cncls  23230  cnpresti  23244  cnprest  23245  cmpsublem  23355  cmpsub  23356  fiuncmp  23360  indisconn  23374  connsub  23377  iunconnlem  23383  islly2  23440  cldllycmp  23451  kgentopon  23494  ptbasfi  23537  ptcnplem  23577  txcnmpt  23580  txcmplem2  23598  hausdiag  23601  txkgen  23608  xkococnlem  23615  qtoptop2  23655  basqtop  23667  fbssfi  23793  filin  23810  infil  23819  fbasrn  23840  fgtr  23846  ufprim  23865  flimrest  23939  txflf  23962  fclsrest  23980  alexsubALTlem4  24006  tsmsres  24100  tsmsxplem1  24109  ustund  24178  trust  24185  utoptop  24190  restutop  24193  cfiluweak  24250  xmetres  24320  metres  24321  blin2  24385  setsmstopn  24434  metrest  24480  ressxms  24481  tgioo  24752  xrsmopn  24769  reconnlem1  24783  xrge0tsms  24791  tcphcph  25205  cfilresi  25263  cfilres  25264  caussi  25265  causs  25266  relcmpcmet  25286  minveclem4a  25398  ismbl2  25496  cmmbl  25503  nulmbl2  25505  unmbl  25506  shftmbl  25507  volinun  25515  voliunlem1  25519  voliunlem2  25520  ioombl1lem4  25530  ioombl1  25531  uniioombllem2  25552  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombl  25558  volivth  25576  vitalilem3  25579  vitalilem4  25580  vitalilem5  25581  vitali  25582  mbfadd  25630  mbfsub  25631  i1fadd  25664  itg1addlem2  25666  itg1addlem4  25668  itg1addlem5  25669  itg1climres  25683  mbfmul  25695  itg2splitlem  25717  itg2split  25718  limcresi  25854  limciun  25863  dvreslem  25878  dvres2lem  25879  dvres  25880  dvres3a  25883  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  ig1peu  26148  pilem2  26430  pilem3  26431  rlimcnp2  26944  ppisval  27082  ppifi  27084  ppiprm  27129  chtprm  27131  chtdif  27136  efchtdvds  27137  ppidif  27141  ppiltx  27155  prmorcht  27156  ppiub  27183  chtlepsi  27185  pclogsum  27194  vmasum  27195  chpval2  27197  chpub  27199  2sqlem8  27405  chebbnd1lem1  27448  chtppilimlem1  27452  rpvmasum2  27491  dchrisum0re  27492  rplogsum  27506  dirith2  27507  nosupbnd1lem1  27688  nosupbnd2  27696  noinfbnd1lem1  27703  axtgcgrrflx  28546  axtgcgrid  28547  axtgsegcon  28548  axtg5seg  28549  axtgbtwnid  28550  axtgpasch  28551  axtgcont1  28552  phnv  30902  minvecolem2  30963  minvecolem3  30964  minvecolem5  30969  minvecolem6  30970  minvecolem7  30971  hlimcaui  31324  chdmm1i  31565  chabs1  31604  chabs2  31605  ledii  31624  lejdii  31626  pjoml4i  31675  cmbr3i  31688  cmbr4i  31689  cmm1i  31694  osumcor2i  31732  3oalem4  31753  pjssmii  31769  pjocini  31786  pjini  31787  mayete3i  31816  riesz4  32152  riesz1  32153  cnlnadjeui  32165  cnlnadjeu  32166  cnlnssadj  32168  nmopadjlei  32176  pjin1i  32280  pjclem1  32283  stji1i  32330  stm1i  32331  dmdbr2  32391  ssmd1  32399  mdslj2i  32408  mdsl2bi  32411  mdslmd1lem1  32413  mdslmd2i  32418  atomli  32470  atcvat4i  32485  sumdmdlem2  32507  dmdbr5ati  32510  dmdbr6ati  32511  dmdbr7ati  32512  indifbi  32607  disjxpin  32675  imadifxp  32688  nfpconfp  32722  off2  32731  ffsrn  32818  indsumin  32954  indf1ofs  32959  gsummptres  33146  xrge0tsmsd  33167  idlinsubrg  33524  ordtrestNEW  34099  qqhnm  34168  qqhcn  34169  rrhre  34199  esumval  34224  esumel  34225  gsumesum  34237  esumlub  34238  esumcst  34241  esumfsup  34248  esumpcvgval  34256  esumcvg  34264  sigainb  34314  ldgenpisyslem1  34341  measinb2  34401  sibfinima  34517  sibfof  34518  eulerpartlemelr  34535  eulerpartlem1  34545  eulerpartgbij  34550  eulerpartlemgu  34555  eulerpartlemgs2  34558  sseqf  34570  ballotlemfelz  34669  ballotlemfp1  34670  reprinrn  34796  reprinfz1  34800  hgt750lemd  34826  bnj1292  34991  connpconn  35451  iccllysconn  35466  cvmsss2  35490  cvmcov2  35491  cvmopnlem  35494  cvmliftmolem2  35498  cvmliftlem15  35514  cvmlift2lem12  35530  mvrsfpw  35722  msrf  35758  elmsta  35764  mthmpps  35798  nepss  35934  dfon2lem4  36000  txpss3v  36092  fixssdm  36120  fixssrn  36121  limitssson  36125  fneer  36569  neibastop1  36575  neibastop2lem  36576  filnetlem3  36596  ontopbas  36644  bj-disj2r  37276  bj-restpw  37345  bj-discrmoore  37364  bj-idres  37415  bj-fvsnun2  37511  bj-ablssgrp  37531  bj-fldssdrng  37543  taupilemrplb  37575  taupilem2  37577  taupi  37578  ptrest  37870  poimirlem29  37900  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  mbfposadd  37918  sstotbnd2  38025  ssbnd  38039  heibor1lem  38060  heiborlem1  38062  heiborlem3  38064  heiborlem5  38066  heiborlem6  38067  heiborlem10  38071  heibor  38072  opidonOLD  38103  exidcl  38127  flddivrng  38250  iss2  38595  xrnss3v  38632  refrelsredund2  38968  lshpinN  39365  lcvexchlem5  39414  pmodlem2  40223  pmod1i  40224  pmodN  40226  osumcllem7N  40338  pexmidlem4N  40349  pl42lem3N  40357  djaclN  41512  dihoml4c  41752  dochdmj1  41766  djhcl  41776  dochexmidlem4  41839  mapd1o  42024  mapdin  42038  unitscyglem5  42569  redvmptabs  42730  elrfi  43051  elrfirn  43052  elrfirn2  43053  ismrcd1  43055  istopclsd  43057  isnacs2  43063  mrefg3  43065  isnacs3  43067  diophrw  43116  diophin  43129  aomclem2  43412  islmodfg  43426  lsmfgcl  43431  lmhmfgima  43441  lmhmfgsplit  43443  lmhmlnmsplit  43444  pwfi2f1o  43453  hbt  43487  ofoafg  43711  harval3  43894  elinintrab  43933  trrelind  44021  clsk3nimkb  44396  isotone2  44405  ismnushort  44657  onfrALTlem2  44902  onfrALTlem2VD  45244  wfac8prim  45358  unirestss  45483  inmap  45567  fsumiunss  45935  islptre  45979  sumnnodd  45990  limclner  46009  liminfval4  46147  liminfval3  46148  cnrefiisplem  46187  cncfuni  46244  ismbl3  46344  ismbl4  46351  fouriersw  46589  qndenserrnbllem  46652  salincl  46682  salgencntex  46701  sge0less  46750  sge0resplit  46764  sge0split  46767  sge0iunmptlemre  46773  carageniuncllem1  46879  carageniuncllem2  46880  caragenel2d  46890  hspmbllem3  46986  hspmbl  46987  ovolval2lem  47001  sssmf  47096  smfaddlem1  47121  smflimlem2  47130  smflimlem3  47131  smflimlem4  47132  smfres  47148  smfmullem4  47152  smfsuplem1  47169  fcoreslem2  47424  rngcrescrhmALTV  48640  rhmsubcALTVlem1  48641  funcringcsetcALTV2lem9  48658  fldcALTV  48692  fldhmsubcALTV  48693  iscnrm3llem2  49309  uptrlem1  49569  uptrlem2  49570  uptrlem3  49571  uptra  49574  uptrar  49575  uobeqw  49578  uptr2  49580  uptr2a  49581  fucoppcfunc  49771  setrec2fun  50051