Theorem inss1 4196

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

Syntax hints:   ∩ cin 3910   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  inss2  4197  ssinss1  4205  unabs  4224  nssinpss  4226  dfin4  4237  inv1  4357  disjdif  4431  ifssun  4502  uniintsn  4945  wefrc  5625  relin1  5766  resss  5961  resmpt3  5998  cnvcnvss  6155  resdmss  6196  resssxp  6231  predss  6270  ordtri3or  6352  onfr  6359  ordelinel  6423  funin  6576  funimass2  6583  fnresin1  6625  fnres  6627  fresin  6711  fresaun  6713  nfvres  6881  ssimaex  6928  fneqeql2  7001  fnfvimad  7190  funiunfv  7204  isoini2  7296  ofrfvalg  7641  ofval  7644  ofrval  7645  off  7651  ofres  7652  ofco  7658  fparlem3  8070  fparlem4  8071  frrlem4  8245  frrlem13  8254  smores  8298  smores2  8300  tfrlem5  8325  pmresg  8820  sbthlem7  9034  sbthcl  9040  infi  9189  imafi  9240  ixpfi2  9277  unifpw  9282  elfiun  9357  dffi3  9358  marypha1lem  9360  ordtypelem6  9452  ordtypelem7  9453  ordtypelem8  9454  wdomima2g  9515  frmin  9678  frrlem15  9686  frrlem16  9687  tskwe  9879  ackbij1lem15  10162  ackbij1lem16  10163  fin23lem23  10255  fin23lem22  10256  fin23lem19  10265  brdom3  10457  brdom5  10458  brdom4  10459  imadomg  10463  fpwwe2lem11  10570  canthp1lem2  10582  wunin  10642  tskin  10688  gruima  10731  ingru  10744  gruina  10747  grur1a  10748  nqerf  10859  nqerrel  10861  hashun3  14325  hashin  14352  hashdif  14354  xptrrel  14922  rexanuz  15288  limsupgle  15419  rlimres  15500  lo1res  15501  lo1resb  15506  rlimresb  15507  o1resb  15508  lo1eq  15510  rlimeq  15511  o1of2  15555  o1rlimmul  15561  isercolllem2  15608  isercolllem3  15609  isercoll  15610  incexclem  15778  incexc  15779  bitsinvp1  16395  sadcaddlem  16403  sadadd2lem  16405  sadadd3  16407  sadaddlem  16412  sadasslem  16416  sadeq  16418  bitsres  16419  smuval2  16428  smupval  16434  smueqlem  16436  smumul  16439  ramub2  16961  ramub1lem2  16974  fvsetsid  17114  ressbasss2  17187  ressinbas  17191  ressress  17193  submre  17542  isacs1i  17598  mreacs  17599  acsfn  17600  invss  17703  sscres  17765  catcisolem  18052  catciso  18053  isacs5lem  18486  psss  18521  tsrss  18530  tsrdir  18545  sylow2a  19533  lsmmod  19589  gsumzres  19823  gsumzaddlem  19835  dprddisj2  19955  ablfac1eu  19989  isunit  20293  rngcbas  20541  rngchomfval  20542  rngccofval  20546  dfrngc2  20548  rnghmsscmap2  20549  rnghmsscmap  20550  rngcsect  20556  funcrngcsetc  20560  ringcbas  20570  ringchomfval  20571  ringccofval  20575  dfringc2  20577  rhmsscmap2  20578  rhmsscmap  20579  rhmsscrnghm  20585  ringcsect  20590  funcringcsetc  20594  rngcrescrhm  20604  rhmsubclem1  20605  fldc  20704  fldhmsubc  20705  acsfn1p  20719  lspextmo  20995  2idlval  21193  pjfval  21648  pjpm  21650  aspsubrg  21818  psrbagsn  22003  ofco2  22371  basdif0  22873  tgval2  22876  eltg3  22882  tgcl  22889  tgdom  22898  tgidm  22900  ppttop  22927  epttop  22929  ntropn  22969  ntrin  22981  mretopd  23012  neiptoptop  23051  restfpw  23099  neitr  23100  restcls  23101  cncls  23194  cnpresti  23208  cnprest  23209  cmpsublem  23319  cmpsub  23320  fiuncmp  23324  indisconn  23338  connsub  23341  iunconnlem  23347  islly2  23404  cldllycmp  23415  kgentopon  23458  ptbasfi  23501  ptcnplem  23541  txcnmpt  23544  txcmplem2  23562  hausdiag  23565  txkgen  23572  xkococnlem  23579  qtoptop2  23619  basqtop  23631  fbssfi  23757  filin  23774  infil  23783  fbasrn  23804  fgtr  23810  ufprim  23829  flimrest  23903  txflf  23926  fclsrest  23944  alexsubALTlem4  23970  tsmsres  24064  tsmsxplem1  24073  ustund  24142  trust  24150  utoptop  24155  restutop  24158  cfiluweak  24215  xmetres  24285  metres  24286  blin2  24350  setsmstopn  24399  metrest  24445  ressxms  24446  tgioo  24717  xrsmopn  24734  reconnlem1  24748  xrge0tsms  24756  tcphcph  25170  cfilresi  25228  cfilres  25229  caussi  25230  causs  25231  relcmpcmet  25251  minveclem4a  25363  ismbl2  25461  cmmbl  25468  nulmbl2  25470  unmbl  25471  shftmbl  25472  volinun  25480  voliunlem1  25484  voliunlem2  25485  ioombl1lem4  25495  ioombl1  25496  uniioombllem2  25517  uniioombllem3  25519  uniioombllem4  25520  uniioombllem5  25521  uniioombl  25523  volivth  25541  vitalilem3  25544  vitalilem4  25545  vitalilem5  25546  vitali  25547  mbfadd  25595  mbfsub  25596  i1fadd  25629  itg1addlem2  25631  itg1addlem4  25633  itg1addlem5  25634  itg1climres  25648  mbfmul  25660  itg2splitlem  25682  itg2split  25683  limcresi  25819  limciun  25828  dvreslem  25843  dvres2lem  25844  dvres  25845  dvres3a  25848  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  ig1peu  26113  pilem2  26395  pilem3  26396  rlimcnp2  26909  ppisval  27047  ppifi  27049  ppiprm  27094  chtprm  27096  chtdif  27101  efchtdvds  27102  ppidif  27106  ppiltx  27120  prmorcht  27121  ppiub  27148  chtlepsi  27150  pclogsum  27159  vmasum  27160  chpval2  27162  chpub  27164  2sqlem8  27370  chebbnd1lem1  27413  chtppilimlem1  27417  rpvmasum2  27456  dchrisum0re  27457  rplogsum  27471  dirith2  27472  nosupbnd1lem1  27653  nosupbnd2  27661  noinfbnd1lem1  27668  axtgcgrrflx  28442  axtgcgrid  28443  axtgsegcon  28444  axtg5seg  28445  axtgbtwnid  28446  axtgpasch  28447  axtgcont1  28448  phnv  30793  minvecolem2  30854  minvecolem3  30855  minvecolem5  30860  minvecolem6  30861  minvecolem7  30862  hlimcaui  31215  chdmm1i  31456  chabs1  31495  chabs2  31496  ledii  31515  lejdii  31517  pjoml4i  31566  cmbr3i  31579  cmbr4i  31580  cmm1i  31585  osumcor2i  31623  3oalem4  31644  pjssmii  31660  pjocini  31677  pjini  31678  mayete3i  31707  riesz4  32043  riesz1  32044  cnlnadjeui  32056  cnlnadjeu  32057  cnlnssadj  32059  nmopadjlei  32067  pjin1i  32171  pjclem1  32174  stji1i  32221  stm1i  32222  dmdbr2  32282  ssmd1  32290  mdslj2i  32299  mdsl2bi  32302  mdslmd1lem1  32304  mdslmd2i  32309  atomli  32361  atcvat4i  32376  sumdmdlem2  32398  dmdbr5ati  32401  dmdbr6ati  32402  dmdbr7ati  32403  indifbi  32499  disjxpin  32567  imadifxp  32580  nfpconfp  32606  off2  32615  ffsrn  32702  indsumin  32835  indf1ofs  32839  gsummptres  33035  xrge0tsmsd  33045  idlinsubrg  33395  ordtrestNEW  33904  qqhnm  33973  qqhcn  33974  rrhre  34004  esumval  34029  esumel  34030  gsumesum  34042  esumlub  34043  esumcst  34046  esumfsup  34053  esumpcvgval  34061  esumcvg  34069  sigainb  34119  ldgenpisyslem1  34146  measinb2  34206  sibfinima  34323  sibfof  34324  eulerpartlemelr  34341  eulerpartlem1  34351  eulerpartgbij  34356  eulerpartlemgu  34361  eulerpartlemgs2  34364  sseqf  34376  ballotlemfelz  34475  ballotlemfp1  34476  reprinrn  34602  reprinfz1  34606  hgt750lemd  34632  bnj1292  34798  connpconn  35215  iccllysconn  35230  cvmsss2  35254  cvmcov2  35255  cvmopnlem  35258  cvmliftmolem2  35262  cvmliftlem15  35278  cvmlift2lem12  35294  mvrsfpw  35486  msrf  35522  elmsta  35528  mthmpps  35562  nepss  35698  dfon2lem4  35767  txpss3v  35859  fixssdm  35887  fixssrn  35888  limitssson  35892  fneer  36334  neibastop1  36340  neibastop2lem  36341  filnetlem3  36361  ontopbas  36409  bj-disj2r  37009  bj-restpw  37073  bj-discrmoore  37092  bj-idres  37141  bj-fvsnun2  37237  bj-ablssgrp  37257  bj-fldssdrng  37269  taupilemrplb  37301  taupilem2  37303  taupi  37304  ptrest  37606  poimirlem29  37636  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  mbfposadd  37654  sstotbnd2  37761  ssbnd  37775  heibor1lem  37796  heiborlem1  37798  heiborlem3  37800  heiborlem5  37802  heiborlem6  37803  heiborlem10  37807  heibor  37808  opidonOLD  37839  exidcl  37863  flddivrng  37986  iss2  38319  xrnss3v  38347  refrelsredund2  38617  lshpinN  38975  lcvexchlem5  39024  pmodlem2  39834  pmod1i  39835  pmodN  39837  osumcllem7N  39949  pexmidlem4N  39960  pl42lem3N  39968  djaclN  41123  dihoml4c  41363  dochdmj1  41377  djhcl  41387  dochexmidlem4  41450  mapd1o  41635  mapdin  41649  unitscyglem5  42180  redvmptabs  42341  elrfi  42675  elrfirn  42676  elrfirn2  42677  ismrcd1  42679  istopclsd  42681  isnacs2  42687  mrefg3  42689  isnacs3  42691  diophrw  42740  diophin  42753  aomclem2  43037  islmodfg  43051  lsmfgcl  43056  lmhmfgima  43066  lmhmfgsplit  43068  lmhmlnmsplit  43069  pwfi2f1o  43078  hbt  43112  ofoafg  43336  harval3  43520  elinintrab  43559  trrelind  43647  clsk3nimkb  44022  isotone2  44031  ismnushort  44283  onfrALTlem2  44529  onfrALTlem2VD  44871  wfac8prim  44985  unirestss  45111  inmap  45196  fsumiunss  45566  islptre  45610  sumnnodd  45621  limclner  45642  liminfval4  45780  liminfval3  45781  cnrefiisplem  45820  cncfuni  45877  ismbl3  45977  ismbl4  45984  fouriersw  46222  qndenserrnbllem  46285  salincl  46315  salgencntex  46334  sge0less  46383  sge0resplit  46397  sge0split  46400  sge0iunmptlemre  46406  carageniuncllem1  46512  carageniuncllem2  46513  caragenel2d  46523  hspmbllem3  46619  hspmbl  46620  ovolval2lem  46634  sssmf  46729  smfaddlem1  46754  smflimlem2  46763  smflimlem3  46764  smflimlem4  46765  smfres  46781  smfmullem4  46785  smfsuplem1  46802  fcoreslem2  47058  rngcrescrhmALTV  48261  rhmsubcALTVlem1  48262  funcringcsetcALTV2lem9  48279  fldcALTV  48313  fldhmsubcALTV  48314  iscnrm3llem2  48931  uptrlem1  49192  uptrlem2  49193  uptrlem3  49194  uptra  49197  uptrar  49198  uobeqw  49201  uptr2  49203  uptr2a  49204  fucoppcfunc  49394  setrec2fun  49674