Theorem inss1 4197

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

Syntax hints:   ∩ cin 3912   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930

This theorem is referenced by:  inss2  4198  ssinss1  4206  ssinss1OLD  4207  unabs  4226  nssinpss  4228  dfin4  4239  inv1  4362  vvin  4372  disjdif  4438  ifssun  4510  uniin  4900  uniintsn  4954  wefrc  5656  relin1  5800  resss  6001  resindm  6030  resmpt3  6041  rnin  6144  cnvcnvssOLD  6194  resdmss  6237  resssxp  6272  predss  6311  ordtri3or  6394  onfr  6401  ordelinel  6465  funin  6613  funimass2  6620  fnresin1  6661  fnres  6663  fresin  6748  fresaun  6750  nfvres  6920  ssimaex  6967  fneqeql2  7043  fnfvimad  7233  funiunfv  7247  isoini2  7338  ofrfvalg  7683  ofval  7686  ofrval  7687  off  7693  ofres  7694  ofco  7700  fparlem3  8108  fparlem4  8109  frrlem4  8285  frrlem13  8294  smores  8338  smores2  8340  tfrlem5  8365  pmresg  8867  sbthlem7  9080  sbthcl  9086  infi  9229  imafi  9274  ixpfi2  9306  unifpw  9311  elfiun  9389  dffi3  9390  marypha1lem  9392  ordtypelem6  9484  ordtypelem7  9485  ordtypelem8  9486  wdomima2g  9547  frmin  9720  frrlem15  9728  frrlem16  9729  tskwe  9935  ackbij1lem15  10215  ackbij1lem16  10216  fin23lem23  10309  fin23lem22  10310  fin23lem19  10319  brdom3  10511  brdom5  10512  brdom4  10513  imadomg  10517  fpwwe2lem11  10625  canthp1lem2  10637  wunin  10697  tskin  10743  gruima  10786  ingru  10799  gruina  10802  grur1a  10803  nqerf  10914  nqerrel  10916  hashun3  14419  hashin  14447  hashdif  14449  xptrrel  15016  rexanuz  15396  limsupgle  15527  rlimres  15608  lo1res  15609  lo1resb  15614  rlimresb  15615  o1resb  15616  lo1eq  15618  rlimeq  15619  o1of2  15663  o1rlimmul  15669  isercolllem2  15716  isercolllem3  15717  isercoll  15718  incexclem  15889  incexc  15890  bitsinvp1  16506  sadcaddlem  16514  sadadd2lem  16516  sadadd3  16518  sadaddlem  16523  sadasslem  16527  sadeq  16529  bitsres  16530  smuval2  16539  smupval  16545  smueqlem  16547  smumul  16550  ramub2  17073  ramub1lem2  17086  fvsetsid  17227  ressbasss2  17300  ressinbas  17304  ressress  17306  submre  17656  isacs1i  17712  mreacs  17713  acsfn  17714  invss  17817  sscres  17879  catcisolem  18166  catciso  18167  isacs5lem  18600  psss  18635  tsrss  18644  tsrdir  18659  sylow2a  19688  lsmmod  19744  gsumzres  19978  gsumzaddlem  19990  dprddisj2  20110  ablfac1eu  20144  isunit  20454  rngcbas  20705  rngchomfval  20706  rngccofval  20710  dfrngc2  20712  rnghmsscmap2  20713  rnghmsscmap  20714  rngcsect  20720  funcrngcsetc  20724  ringcbas  20734  ringchomfval  20735  ringccofval  20739  dfringc2  20741  rhmsscmap2  20742  rhmsscmap  20743  rhmsscrnghm  20749  ringcsect  20754  funcringcsetc  20758  rngcrescrhm  20768  rhmsubclem1  20769  fldc  20864  fldhmsubc  20865  acsfn1p  20879  lspextmo  21154  2idlval  21360  pjfval  21824  pjpm  21826  aspsubrg  21993  psrbagsn  22182  ofco2  22576  basdif0  23078  tgval2  23081  eltg3  23087  tgcl  23094  tgdom  23103  tgidm  23105  ppttop  23132  epttop  23134  ntropn  23174  ntrin  23186  mretopd  23217  neiptoptop  23256  restfpw  23304  neitr  23305  restcls  23306  cncls  23399  cnpresti  23413  cnprest  23414  cmpsublem  23524  cmpsub  23525  fiuncmp  23529  indisconn  23543  connsub  23546  iunconnlem  23552  islly2  23609  cldllycmp  23620  kgentopon  23663  ptbasfi  23706  ptcnplem  23746  txcnmpt  23749  txcmplem2  23767  hausdiag  23770  txkgen  23777  xkococnlem  23784  qtoptop2  23824  basqtop  23836  fbssfi  23962  filin  23979  infil  23988  fbasrn  24009  fgtr  24015  ufprim  24034  flimrest  24108  txflf  24131  fclsrest  24149  alexsubALTlem4  24175  tsmsres  24269  tsmsxplem1  24278  ustund  24347  trust  24354  utoptop  24359  restutop  24362  cfiluweak  24419  xmetres  24489  metres  24490  blin2  24554  setsmstopn  24603  metrest  24649  ressxms  24650  tgioo  24921  xrsmopn  24938  reconnlem1  24952  xrge0tsms  24960  tcphcph  25364  cfilresi  25422  cfilres  25423  caussi  25424  causs  25425  relcmpcmet  25445  minveclem4a  25557  ismbl2  25654  cmmbl  25661  nulmbl2  25663  unmbl  25664  shftmbl  25665  volinun  25673  voliunlem1  25677  voliunlem2  25678  ioombl1lem4  25688  ioombl1  25689  uniioombllem2  25710  uniioombllem3  25712  uniioombllem4  25713  uniioombllem5  25714  uniioombl  25716  volivth  25734  vitalilem3  25737  vitalilem4  25738  vitalilem5  25739  vitali  25740  mbfadd  25788  mbfsub  25789  i1fadd  25822  itg1addlem2  25824  itg1addlem4  25826  itg1addlem5  25827  itg1climres  25841  mbfmul  25853  itg2splitlem  25875  itg2split  25876  limcresi  26012  limciun  26021  dvreslem  26036  dvres2lem  26037  dvres  26038  dvres3a  26041  dvaddbr  26065  dvmulbr  26066  dvfsumle  26148  dvfsumabs  26150  ig1peu  26300  pilem2  26580  pilem3  26581  rlimcnp2  27096  ppisval  27233  ppifi  27235  ppiprm  27280  chtprm  27282  chtdif  27287  efchtdvds  27288  ppidif  27292  ppiltx  27306  prmorcht  27307  ppiub  27333  chtlepsi  27335  pclogsum  27344  vmasum  27345  chpval2  27347  chpub  27349  2sqlem8  27555  chebbnd1lem1  27598  chtppilimlem1  27602  rpvmasum2  27641  dchrisum0re  27642  rplogsum  27656  dirith2  27657  nosupbnd1lem1  27837  nosupbnd2  27845  noinfbnd1lem1  27852  axtgcgrrflx  28696  axtgcgrid  28697  axtgsegcon  28698  axtg5seg  28699  axtgbtwnid  28700  axtgpasch  28701  axtgcont1  28702  phnv  31106  minvecolem2  31167  minvecolem3  31168  minvecolem5  31173  minvecolem6  31174  minvecolem7  31175  hlimcaui  31528  chdmm1i  31769  chabs1  31808  chabs2  31809  ledii  31828  lejdii  31830  pjoml4i  31879  cmbr3i  31892  cmbr4i  31893  cmm1i  31898  osumcor2i  31936  3oalem4  31957  pjssmii  31973  pjocini  31990  pjini  31991  mayete3i  32020  riesz4  32356  riesz1  32357  cnlnadjeui  32369  cnlnadjeu  32370  cnlnssadj  32372  nmopadjlei  32380  pjin1i  32484  pjclem1  32487  stji1i  32534  stm1i  32535  dmdbr2  32595  ssmd1  32603  mdslj2i  32612  mdsl2bi  32615  mdslmd1lem1  32617  mdslmd2i  32622  atomli  32674  atcvat4i  32689  sumdmdlem2  32711  dmdbr5ati  32714  dmdbr6ati  32715  dmdbr7ati  32716  indifbi  32806  disjxpin  32873  imadifxp  32886  nfpconfp  32917  off2  32926  ffsrn  33013  indsumin  33121  indf1ofs  33126  gsummptres  33312  xrge0tsmsd  33333  idlinsubrg  33682  ordtrestNEW  34255  qqhnm  34324  qqhcn  34325  rrhre  34355  esumval  34380  esumel  34381  gsumesum  34393  esumlub  34394  esumcst  34397  esumfsup  34404  esumpcvgval  34412  esumcvg  34420  sigainb  34470  ldgenpisyslem1  34497  measinb2  34557  sibfinima  34673  sibfof  34674  eulerpartlemelr  34691  eulerpartlem1  34701  eulerpartgbij  34706  eulerpartlemgu  34711  eulerpartlemgs2  34714  sseqf  34726  ballotlemfelz  34825  ballotlemfp1  34826  reprinrn  34949  reprinfz1  34953  hgt750lemd  34979  bnj1292  35147  connpconn  35625  iccllysconn  35640  cvmsss2  35664  cvmcov2  35665  cvmopnlem  35668  cvmliftmolem2  35672  cvmliftlem15  35688  cvmlift2lem12  35704  mvrsfpw  35896  msrf  35932  elmsta  35938  mthmpps  35972  nepss  36108  dfon2lem4  36174  txpss3v  36266  fixssdm  36294  fixssrn  36295  limitssson  36299  fneer  36752  neibastop1  36758  neibastop2lem  36759  filnetlem3  36779  ontopbas  36827  bj-disj2r  37551  bj-restpw  37621  bj-discrmoore  37640  bj-idres  37691  bj-fvsnun2  37787  bj-ablssgrp  37807  bj-fldssdrng  37819  taupilemrplb  37851  taupilem2  37853  taupi  37854  ptrest  38157  poimirlem29  38187  mblfinlem3  38197  mblfinlem4  38198  ismblfin  38199  mbfposadd  38205  sstotbnd2  38312  ssbnd  38326  heibor1lem  38347  heiborlem1  38349  heiborlem3  38351  heiborlem5  38353  heiborlem6  38354  heiborlem10  38358  heibor  38359  opidonOLD  38390  exidcl  38414  flddivrng  38537  iss2  38882  xrnss3v  38919  refrelsredund2  39255  lshpinN  39652  lcvexchlem5  39701  pmodlem2  40510  pmod1i  40511  pmodN  40513  osumcllem7N  40625  pexmidlem4N  40636  pl42lem3N  40644  djaclN  41799  dihoml4c  42039  dochdmj1  42053  djhcl  42063  dochexmidlem4  42126  mapd1o  42311  mapdin  42325  unitscyglem5  42855  redvmptabs  43010  elrfi  43316  elrfirn  43317  elrfirn2  43318  ismrcd1  43320  istopclsd  43322  isnacs2  43328  mrefg3  43330  isnacs3  43332  diophrw  43381  diophin  43394  aomclem2  43673  islmodfg  43687  lsmfgcl  43692  lmhmfgima  43702  lmhmfgsplit  43704  lmhmlnmsplit  43705  pwfi2f1o  43714  hbt  43748  ofoafg  43972  harval3  44155  elinintrab  44194  trrelind  44282  clsk3nimkb  44657  isotone2  44666  ismnushort  44902  onfrALTlem2  45146  onfrALTlem2VD  45488  wfac8prim  45602  unirestss  45733  inmap  45816  fsumiunss  46182  islptre  46226  sumnnodd  46237  limclner  46256  liminfval4  46394  liminfval3  46395  cnrefiisplem  46434  cncfuni  46491  ismbl3  46591  ismbl4  46598  fouriersw  46836  qndenserrnbllem  46899  salincl  46929  salgencntex  46948  sge0less  46997  sge0resplit  47011  sge0split  47014  sge0iunmptlemre  47020  carageniuncllem1  47126  carageniuncllem2  47127  caragenel2d  47137  hspmbllem3  47233  hspmbl  47234  ovolval2lem  47248  sssmf  47343  smfaddlem1  47368  smflimlem2  47377  smflimlem3  47378  smflimlem4  47379  smfres  47395  smfmullem4  47399  smfsuplem1  47416  fcoreslem2  47689  indprmfz  48270  ppivalnn  48272  rngcrescrhmALTV  48933  rhmsubcALTVlem1  48934  funcringcsetcALTV2lem9  48951  fldcALTV  48985  fldhmsubcALTV  48986  iscnrm3llem2  49612  uptrlem1  49872  uptrlem2  49873  uptrlem3  49874  uptra  49877  uptrar  49878  uobeqw  49881  uptr2  49883  uptr2a  49884  fucoppcfunc  50074  setrec2fun  50354