Theorem inss1 4182

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

This proof depends on syntax axioms:   ∩ cin 3898   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  inss2  4183  ssinss1  4191  ssinss1OLD  4192  unabs  4211  nssinpss  4213  dfin4  4224  inv1  4348  vvin  4359  ifssun  4500  uniin  4891  uniintsn  4945  wefrc  5645  relin1  5790  resss  5992  resindm  6019  resmpt3  6030  rnin  6137  cnvcnvssOLD  6187  resdmss  6236  resssxp  6272  predss  6312  ordtri3or  6395  onfr  6402  ordelinel  6466  funin  6616  funimass2  6623  fnresin1  6664  fnres  6666  fresin  6751  fresaun  6753  nfvres  6923  ssimaex  6970  fneqeql2  7046  fnfvimad  7240  funiunfv  7252  isoini2  7347  ofrfvalg  7701  ofval  7704  ofrval  7705  off  7711  ofres  7712  ofco  7718  fparlem3  8125  fparlem4  8126  frrlem4  8307  frrlem13  8316  smores  8360  smores2  8362  tfrlem5  8387  pmresg  8898  sbthlem7  9112  sbthcl  9118  infi  9261  imafi  9307  ixpfi2  9339  unifpw  9344  elfiun  9422  dffi3  9423  marypha1lem  9425  ordtypelem6  9517  ordtypelem7  9518  ordtypelem8  9519  wdomima2g  9580  frmin  9753  frrlem15  9761  frrlem16  9762  setrec2fun  9973  tskwe  10031  ackbij1lem15  10311  ackbij1lem16  10312  fin23lem23  10404  fin23lem22  10405  fin23lem19  10414  brdom3  10607  brdom5  10608  brdom4  10609  imadomg  10613  imadomnum  10614  fpwwe2lem11  10726  canthp1lem2  10738  wunin  10798  tskin  10844  gruima  10887  ingru  10900  gruina  10903  grur1a  10904  nqerf  11015  nqerrel  11017  hashun3  14528  hashin  14556  hashdif  14558  xptrrel  15133  rexanuz  15513  limsupgle  15644  rlimres  15725  lo1res  15726  lo1resb  15731  rlimresb  15732  o1resb  15733  lo1eq  15735  rlimeq  15736  o1of2  15780  o1rlimmul  15786  isercolllem2  15833  isercolllem3  15834  isercoll  15835  incexclem  16005  incexc  16006  bitsinvp1  16619  sadcaddlem  16627  sadadd2lem  16629  sadadd3  16631  sadaddlem  16636  sadasslem  16640  sadeq  16642  bitsres  16643  smuval2  16652  smupval  16658  smueqlem  16660  smumul  16663  ramub2  17192  ramub1lem2  17205  fvsetsid  17346  ressbasss2  17419  ressinbas  17423  ressress  17425  submre  17775  isacs1i  17831  mreacs  17832  acsfn  17833  invss  17936  sscres  17998  catcisolem  18285  catciso  18286  isacs5lem  18719  psss  18754  tsrss  18763  tsrdir  18778  sylow2a  19833  lsmmod  19889  gsumzres  20123  gsumzaddlem  20135  dprddisj2  20255  ablfac1eu  20289  isunit  20603  rngcbas  20873  rngchomfval  20874  rngccofval  20878  dfrngc2  20880  rnghmsscmap2  20881  rnghmsscmap  20882  rngcsect  20888  funcrngcsetc  20892  ringcbas  20902  ringchomfval  20903  ringccofval  20907  dfringc2  20909  rhmsscmap2  20910  rhmsscmap  20911  rhmsscrnghm  20917  ringcsect  20922  funcringcsetc  20926  rngcrescrhm  20936  rhmsubclem1  20937  fldc  21041  fldhmsubc  21042  acsfn1p  21056  lspextmo  21331  2idlval  21544  pjfval  22012  pjpm  22014  aspsubrg  22183  psrbagsn  22372  ofco2  22766  basdif0  23271  tgval2  23274  eltg3  23280  tgcl  23287  tgdom  23296  tgidm  23298  ppttop  23325  epttop  23327  ntropn  23367  ntrin  23379  mretopd  23410  neiptoptop  23449  restfpw  23497  neitr  23498  restcls  23499  cncls  23592  cnpresti  23606  cnprest  23607  cmpsublem  23717  cmpsub  23718  fiuncmp  23722  indisconn  23736  connsub  23739  iunconnlem  23745  islly2  23803  cldllycmp  23814  kgentopon  23857  ptbasfi  23900  ptcnplem  23940  txcnmpt  23943  txcmplem2  23961  hausdiag  23964  txkgen  23971  xkococnlem  23978  qtoptop2  24018  basqtop  24030  fbssfi  24156  filin  24173  infil  24182  fbasrn  24203  fgtr  24209  ufprim  24228  flimrest  24302  txflf  24325  fclsrest  24343  alexsubALTlem4  24369  tsmsres  24463  tsmsxplem1  24472  ustund  24541  trust  24548  utoptop  24553  restutop  24556  cfiluweak  24613  xmetres  24683  metres  24684  blin2  24748  setsmstopn  24797  metrest  24843  ressxms  24844  tgioo  25115  xrsmopn  25132  reconnlem1  25146  xrge0tsms  25154  tcphcph  25558  cfilresi  25616  cfilres  25617  caussi  25618  causs  25619  relcmpcmet  25639  minveclem4a  25751  ismbl2  25848  cmmbl  25855  nulmbl2  25857  unmbl  25858  shftmbl  25859  volinun  25867  voliunlem1  25871  voliunlem2  25872  ioombl1lem4  25882  ioombl1  25883  uniioombllem2  25904  uniioombllem3  25906  uniioombllem4  25907  uniioombllem5  25908  uniioombl  25910  volivth  25928  vitalilem3  25931  vitalilem4  25932  vitalilem5  25933  vitali  25934  mbfadd  25982  mbfsub  25983  i1fadd  26016  itg1addlem2  26018  itg1addlem4  26020  itg1addlem5  26021  itg1climres  26035  mbfmul  26047  itg2splitlem  26069  itg2split  26070  limcresi  26205  limciun  26214  dvreslem  26229  dvres2lem  26230  dvres  26231  dvres3a  26234  dvaddbr  26258  dvmulbr  26259  dvfsumle  26341  dvfsumabs  26343  ig1peu  26493  pilem2  26779  pilem3  26780  rlimcnp2  27294  ppisval  27431  ppifi  27433  ppiprm  27478  chtprm  27480  chtdif  27485  efchtdvds  27486  ppidif  27490  ppiltx  27504  prmorcht  27505  ppiub  27531  chtlepsi  27533  pclogsum  27542  vmasum  27543  chpval2  27545  chpub  27547  2sqlem8  27753  chebbnd1lem1  27796  chtppilimlem1  27800  rpvmasum2  27839  dchrisum0re  27840  rplogsum  27854  dirith2  27855  nosupbnd1lem1  28065  nosupbnd2  28073  noinfbnd1lem1  28080  axtgcgrrflx  28924  axtgcgrid  28925  axtgsegcon  28926  axtg5seg  28927  axtgbtwnid  28928  axtgpasch  28929  axtgcont1  28930  phnv  31416  minvecolem2  31477  minvecolem3  31478  minvecolem5  31483  minvecolem6  31484  minvecolem7  31485  hlimcaui  31838  chdmm1i  32079  chabs1  32118  chabs2  32119  ledii  32138  lejdii  32140  pjoml4i  32189  cmbr3i  32202  cmbr4i  32203  cmm1i  32208  osumcor2i  32246  3oalem4  32267  pjssmii  32283  pjocini  32300  pjini  32301  mayete3i  32330  riesz4  32666  riesz1  32667  cnlnadjeui  32679  cnlnadjeu  32680  cnlnssadj  32682  nmopadjlei  32690  pjin1i  32794  pjclem1  32797  stji1i  32844  stm1i  32845  dmdbr2  32905  ssmd1  32913  mdslj2i  32922  mdsl2bi  32925  mdslmd1lem1  32927  mdslmd2i  32932  atomli  32984  atcvat4i  32999  sumdmdlem2  33021  dmdbr5ati  33024  dmdbr6ati  33025  dmdbr7ati  33026  indifbi  33116  disjxpin  33182  imadifxp  33195  nfpconfp  33226  off2  33235  ffsrn  33320  indsumin  33428  indf1ofs  33433  gsummptres  33613  xrge0tsmsd  33634  idlinsubrg  33981  ordtrestNEW  34553  qqhnm  34622  qqhcn  34623  rrhre  34653  esumval  34678  esumel  34679  gsumesum  34691  esumlub  34692  esumcst  34695  esumfsup  34702  esumpcvgval  34710  esumcvg  34718  sigainb  34769  ldgenpisyslem1  34796  measinb2  34856  sibfinima  34971  sibfof  34972  eulerpartlemelr  34989  eulerpartlem1  34999  eulerpartgbij  35004  eulerpartlemgu  35009  eulerpartlemgs2  35012  sseqf  35024  ballotlemfelz  35123  ballotlemfp1  35124  reprinrn  35247  reprinfz1  35251  hgt750lemd  35277  bnj1292  35445  connpconn  36000  iccllysconn  36015  cvmsss2  36039  cvmcov2  36040  cvmopnlem  36043  cvmliftmolem2  36047  cvmliftlem15  36063  cvmlift2lem12  36079  mvrsfpw  36271  msrf  36307  elmsta  36313  mthmpps  36347  nepss  36483  dfon2lem4  36548  txpss3v  36640  fixssdm  36668  fixssrn  36669  limitssson  36673  fneer  37141  neibastop1  37147  neibastop2lem  37148  filnetlem3  37168  ontopbas  37216  bj-disj2r  37941  bj-restpw  38013  bj-discrmoore  38032  bj-idres  38081  bj-fvsnun2  38177  bj-ablssgrp  38197  bj-fldssdrng  38209  taupilemrplb  38241  taupilem2  38243  taupi  38244  ptrest  38537  poimirlem29  38567  mblfinlem3  38577  mblfinlem4  38578  ismblfin  38579  mbfposadd  38585  sstotbnd2  38708  ssbnd  38722  heibor1lem  38743  heiborlem1  38745  heiborlem3  38747  heiborlem5  38749  heiborlem6  38750  heiborlem10  38754  heibor  38755  opidonOLD  38786  exidcl  38810  flddivrng  38933  iss2  39276  xrnss3v  39313  refrelsredund2  39649  lshpinN  40046  lcvexchlem5  40095  pmodlem2  40904  pmod1i  40905  pmodN  40907  osumcllem7N  41019  pexmidlem4N  41030  pl42lem3N  41038  djaclN  42193  dihoml4c  42433  dochdmj1  42447  djhcl  42457  dochexmidlem4  42520  mapd1o  42705  mapdin  42719  unitscyglem5  43249  redvmptabs  43411  elrfi  43704  elrfirn  43705  elrfirn2  43706  ismrcd1  43708  istopclsd  43710  isnacs2  43716  mrefg3  43718  isnacs3  43720  diophrw  43769  diophin  43782  aomclem2  44056  islmodfg  44070  lsmfgcl  44075  lmhmfgima  44085  lmhmfgsplit  44087  lmhmlnmsplit  44088  pwfi2f1o  44097  hbt  44131  ofoafg  44355  harval3  44538  elinintrab  44577  trrelind  44664  clsk3nimkb  45039  isotone2  45048  ismnushort  45284  onfrALTlem2  45528  onfrALTlem2VD  45870  wfac8prim  45991  unirestss  46138  inmap  46221  fsumiunss  46586  islptre  46630  sumnnodd  46641  limclner  46660  liminfval4  46798  liminfval3  46799  cnrefiisplem  46838  cncfuni  46895  ismbl3  46995  ismbl4  47002  fouriersw  47240  qndenserrnbllem  47303  salincl  47333  salgencntex  47352  sge0less  47401  sge0resplit  47415  sge0split  47418  sge0iunmptlemre  47424  carageniuncllem1  47530  carageniuncllem2  47531  caragenel2d  47541  hspmbllem3  47637  hspmbl  47638  ovolval2lem  47652  sssmf  47747  smfaddlem1  47772  smflimlem2  47781  smflimlem3  47782  smflimlem4  47783  smfres  47799  smfmullem4  47803  smfsuplem1  47820  wrddrin  47896  chndrin  47901  chnrrin  47906  fcoreslem2  48133  indprmfz  48714  ppivalnn  48716  rngcrescrhmALTV  49376  rhmsubcALTVlem1  49377  funcringcsetcALTV2lem9  49394  fldcALTV  49428  fldhmsubcALTV  49429  iscnrm3llem2  50057  uptrlem1  50317  uptrlem2  50318  uptrlem3  50319  uptra  50322  uptrar  50323  uobeqw  50326  uptr2  50328  uptr2a  50329  fucoppcfunc  50519