Theorem inss1 4189

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

Syntax hints:   ∩ cin 3900   ⊆ wss 3901

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  inss2  4190  ssinss1  4198  unabs  4217  nssinpss  4219  dfin4  4230  inv1  4350  disjdif  4424  ifssun  4497  uniintsn  4940  wefrc  5618  relin1  5761  resss  5960  resmpt3  5997  cnvcnvss  6152  resdmss  6193  resssxp  6228  predss  6267  ordtri3or  6349  onfr  6356  ordelinel  6420  funin  6568  funimass2  6575  fnresin1  6617  fnres  6619  fresin  6703  fresaun  6705  nfvres  6872  ssimaex  6919  fneqeql2  6992  fnfvimad  7180  funiunfv  7194  isoini2  7285  ofrfvalg  7630  ofval  7633  ofrval  7634  off  7640  ofres  7641  ofco  7647  fparlem3  8056  fparlem4  8057  frrlem4  8231  frrlem13  8240  smores  8284  smores2  8286  tfrlem5  8311  pmresg  8808  sbthlem7  9021  sbthcl  9027  infi  9170  imafi  9215  ixpfi2  9250  unifpw  9255  elfiun  9333  dffi3  9334  marypha1lem  9336  ordtypelem6  9428  ordtypelem7  9429  ordtypelem8  9430  wdomima2g  9491  frmin  9661  frrlem15  9669  frrlem16  9670  tskwe  9862  ackbij1lem15  10143  ackbij1lem16  10144  fin23lem23  10236  fin23lem22  10237  fin23lem19  10246  brdom3  10438  brdom5  10439  brdom4  10440  imadomg  10444  fpwwe2lem11  10552  canthp1lem2  10564  wunin  10624  tskin  10670  gruima  10713  ingru  10726  gruina  10729  grur1a  10730  nqerf  10841  nqerrel  10843  hashun3  14307  hashin  14334  hashdif  14336  xptrrel  14903  rexanuz  15269  limsupgle  15400  rlimres  15481  lo1res  15482  lo1resb  15487  rlimresb  15488  o1resb  15489  lo1eq  15491  rlimeq  15492  o1of2  15536  o1rlimmul  15542  isercolllem2  15589  isercolllem3  15590  isercoll  15591  incexclem  15759  incexc  15760  bitsinvp1  16376  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  sadeq  16399  bitsres  16400  smuval2  16409  smupval  16415  smueqlem  16417  smumul  16420  ramub2  16942  ramub1lem2  16955  fvsetsid  17095  ressbasss2  17168  ressinbas  17172  ressress  17174  submre  17524  isacs1i  17580  mreacs  17581  acsfn  17582  invss  17685  sscres  17747  catcisolem  18034  catciso  18035  isacs5lem  18468  psss  18503  tsrss  18512  tsrdir  18527  sylow2a  19548  lsmmod  19604  gsumzres  19838  gsumzaddlem  19850  dprddisj2  19970  ablfac1eu  20004  isunit  20309  rngcbas  20554  rngchomfval  20555  rngccofval  20559  dfrngc2  20561  rnghmsscmap2  20562  rnghmsscmap  20563  rngcsect  20569  funcrngcsetc  20573  ringcbas  20583  ringchomfval  20584  ringccofval  20588  dfringc2  20590  rhmsscmap2  20591  rhmsscmap  20592  rhmsscrnghm  20598  ringcsect  20603  funcringcsetc  20607  rngcrescrhm  20617  rhmsubclem1  20618  fldc  20717  fldhmsubc  20718  acsfn1p  20732  lspextmo  21008  2idlval  21206  pjfval  21661  pjpm  21663  aspsubrg  21831  psrbagsn  22018  ofco2  22395  basdif0  22897  tgval2  22900  eltg3  22906  tgcl  22913  tgdom  22922  tgidm  22924  ppttop  22951  epttop  22953  ntropn  22993  ntrin  23005  mretopd  23036  neiptoptop  23075  restfpw  23123  neitr  23124  restcls  23125  cncls  23218  cnpresti  23232  cnprest  23233  cmpsublem  23343  cmpsub  23344  fiuncmp  23348  indisconn  23362  connsub  23365  iunconnlem  23371  islly2  23428  cldllycmp  23439  kgentopon  23482  ptbasfi  23525  ptcnplem  23565  txcnmpt  23568  txcmplem2  23586  hausdiag  23589  txkgen  23596  xkococnlem  23603  qtoptop2  23643  basqtop  23655  fbssfi  23781  filin  23798  infil  23807  fbasrn  23828  fgtr  23834  ufprim  23853  flimrest  23927  txflf  23950  fclsrest  23968  alexsubALTlem4  23994  tsmsres  24088  tsmsxplem1  24097  ustund  24166  trust  24173  utoptop  24178  restutop  24181  cfiluweak  24238  xmetres  24308  metres  24309  blin2  24373  setsmstopn  24422  metrest  24468  ressxms  24469  tgioo  24740  xrsmopn  24757  reconnlem1  24771  xrge0tsms  24779  tcphcph  25193  cfilresi  25251  cfilres  25252  caussi  25253  causs  25254  relcmpcmet  25274  minveclem4a  25386  ismbl2  25484  cmmbl  25491  nulmbl2  25493  unmbl  25494  shftmbl  25495  volinun  25503  voliunlem1  25507  voliunlem2  25508  ioombl1lem4  25518  ioombl1  25519  uniioombllem2  25540  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombl  25546  volivth  25564  vitalilem3  25567  vitalilem4  25568  vitalilem5  25569  vitali  25570  mbfadd  25618  mbfsub  25619  i1fadd  25652  itg1addlem2  25654  itg1addlem4  25656  itg1addlem5  25657  itg1climres  25671  mbfmul  25683  itg2splitlem  25705  itg2split  25706  limcresi  25842  limciun  25851  dvreslem  25866  dvres2lem  25867  dvres  25868  dvres3a  25871  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  ig1peu  26136  pilem2  26418  pilem3  26419  rlimcnp2  26932  ppisval  27070  ppifi  27072  ppiprm  27117  chtprm  27119  chtdif  27124  efchtdvds  27125  ppidif  27129  ppiltx  27143  prmorcht  27144  ppiub  27171  chtlepsi  27173  pclogsum  27182  vmasum  27183  chpval2  27185  chpub  27187  2sqlem8  27393  chebbnd1lem1  27436  chtppilimlem1  27440  rpvmasum2  27479  dchrisum0re  27480  rplogsum  27494  dirith2  27495  nosupbnd1lem1  27676  nosupbnd2  27684  noinfbnd1lem1  27691  axtgcgrrflx  28534  axtgcgrid  28535  axtgsegcon  28536  axtg5seg  28537  axtgbtwnid  28538  axtgpasch  28539  axtgcont1  28540  phnv  30889  minvecolem2  30950  minvecolem3  30951  minvecolem5  30956  minvecolem6  30957  minvecolem7  30958  hlimcaui  31311  chdmm1i  31552  chabs1  31591  chabs2  31592  ledii  31611  lejdii  31613  pjoml4i  31662  cmbr3i  31675  cmbr4i  31676  cmm1i  31681  osumcor2i  31719  3oalem4  31740  pjssmii  31756  pjocini  31773  pjini  31774  mayete3i  31803  riesz4  32139  riesz1  32140  cnlnadjeui  32152  cnlnadjeu  32153  cnlnssadj  32155  nmopadjlei  32163  pjin1i  32267  pjclem1  32270  stji1i  32317  stm1i  32318  dmdbr2  32378  ssmd1  32386  mdslj2i  32395  mdsl2bi  32398  mdslmd1lem1  32400  mdslmd2i  32405  atomli  32457  atcvat4i  32472  sumdmdlem2  32494  dmdbr5ati  32497  dmdbr6ati  32498  dmdbr7ati  32499  indifbi  32595  disjxpin  32663  imadifxp  32676  nfpconfp  32710  off2  32719  ffsrn  32807  indsumin  32943  indf1ofs  32948  gsummptres  33135  xrge0tsmsd  33155  idlinsubrg  33512  ordtrestNEW  34078  qqhnm  34147  qqhcn  34148  rrhre  34178  esumval  34203  esumel  34204  gsumesum  34216  esumlub  34217  esumcst  34220  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  sigainb  34293  ldgenpisyslem1  34320  measinb2  34380  sibfinima  34496  sibfof  34497  eulerpartlemelr  34514  eulerpartlem1  34524  eulerpartgbij  34529  eulerpartlemgu  34534  eulerpartlemgs2  34537  sseqf  34549  ballotlemfelz  34648  ballotlemfp1  34649  reprinrn  34775  reprinfz1  34779  hgt750lemd  34805  bnj1292  34971  connpconn  35429  iccllysconn  35444  cvmsss2  35468  cvmcov2  35469  cvmopnlem  35472  cvmliftmolem2  35476  cvmliftlem15  35492  cvmlift2lem12  35508  mvrsfpw  35700  msrf  35736  elmsta  35742  mthmpps  35776  nepss  35912  dfon2lem4  35978  txpss3v  36070  fixssdm  36098  fixssrn  36099  limitssson  36103  fneer  36547  neibastop1  36553  neibastop2lem  36554  filnetlem3  36574  ontopbas  36622  bj-disj2r  37229  bj-restpw  37297  bj-discrmoore  37316  bj-idres  37365  bj-fvsnun2  37461  bj-ablssgrp  37481  bj-fldssdrng  37493  taupilemrplb  37525  taupilem2  37527  taupi  37528  ptrest  37820  poimirlem29  37850  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  mbfposadd  37868  sstotbnd2  37975  ssbnd  37989  heibor1lem  38010  heiborlem1  38012  heiborlem3  38014  heiborlem5  38016  heiborlem6  38017  heiborlem10  38021  heibor  38022  opidonOLD  38053  exidcl  38077  flddivrng  38200  iss2  38537  xrnss3v  38566  refrelsredund2  38890  lshpinN  39249  lcvexchlem5  39298  pmodlem2  40107  pmod1i  40108  pmodN  40110  osumcllem7N  40222  pexmidlem4N  40233  pl42lem3N  40241  djaclN  41396  dihoml4c  41636  dochdmj1  41650  djhcl  41660  dochexmidlem4  41723  mapd1o  41908  mapdin  41922  unitscyglem5  42453  redvmptabs  42615  elrfi  42936  elrfirn  42937  elrfirn2  42938  ismrcd1  42940  istopclsd  42942  isnacs2  42948  mrefg3  42950  isnacs3  42952  diophrw  43001  diophin  43014  aomclem2  43297  islmodfg  43311  lsmfgcl  43316  lmhmfgima  43326  lmhmfgsplit  43328  lmhmlnmsplit  43329  pwfi2f1o  43338  hbt  43372  ofoafg  43596  harval3  43779  elinintrab  43818  trrelind  43906  clsk3nimkb  44281  isotone2  44290  ismnushort  44542  onfrALTlem2  44787  onfrALTlem2VD  45129  wfac8prim  45243  unirestss  45368  inmap  45453  fsumiunss  45821  islptre  45865  sumnnodd  45876  limclner  45895  liminfval4  46033  liminfval3  46034  cnrefiisplem  46073  cncfuni  46130  ismbl3  46230  ismbl4  46237  fouriersw  46475  qndenserrnbllem  46538  salincl  46568  salgencntex  46587  sge0less  46636  sge0resplit  46650  sge0split  46653  sge0iunmptlemre  46659  carageniuncllem1  46765  carageniuncllem2  46766  caragenel2d  46776  hspmbllem3  46872  hspmbl  46873  ovolval2lem  46887  sssmf  46982  smfaddlem1  47007  smflimlem2  47016  smflimlem3  47017  smflimlem4  47018  smfres  47034  smfmullem4  47038  smfsuplem1  47055  fcoreslem2  47310  rngcrescrhmALTV  48526  rhmsubcALTVlem1  48527  funcringcsetcALTV2lem9  48544  fldcALTV  48578  fldhmsubcALTV  48579  iscnrm3llem2  49195  uptrlem1  49455  uptrlem2  49456  uptrlem3  49457  uptra  49460  uptrar  49461  uobeqw  49464  uptr2  49466  uptr2a  49467  fucoppcfunc  49657  setrec2fun  49937