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  17594  mreacs  17595  acsfn  17596  invss  17699  sscres  17761  catcisolem  18048  catciso  18049  isacs5lem  18480  psss  18515  tsrss  18524  tsrdir  18539  sylow2a  19525  lsmmod  19581  gsumzres  19815  gsumzaddlem  19827  dprddisj2  19947  ablfac1eu  19981  isunit  20258  rngcbas  20506  rngchomfval  20507  rngccofval  20511  dfrngc2  20513  rnghmsscmap2  20514  rnghmsscmap  20515  rngcsect  20521  funcrngcsetc  20525  ringcbas  20535  ringchomfval  20536  ringccofval  20540  dfringc2  20542  rhmsscmap2  20543  rhmsscmap  20544  rhmsscrnghm  20550  ringcsect  20555  funcringcsetc  20559  rngcrescrhm  20569  rhmsubclem1  20570  fldc  20669  fldhmsubc  20670  acsfn1p  20684  lspextmo  20939  2idlval  21137  pjfval  21591  pjpm  21593  aspsubrg  21761  psrbagsn  21946  ofco2  22314  basdif0  22816  tgval2  22819  eltg3  22825  tgcl  22832  tgdom  22841  tgidm  22843  ppttop  22870  epttop  22872  ntropn  22912  ntrin  22924  mretopd  22955  neiptoptop  22994  restfpw  23042  neitr  23043  restcls  23044  cncls  23137  cnpresti  23151  cnprest  23152  cmpsublem  23262  cmpsub  23263  fiuncmp  23267  indisconn  23281  connsub  23284  iunconnlem  23290  islly2  23347  cldllycmp  23358  kgentopon  23401  ptbasfi  23444  ptcnplem  23484  txcnmpt  23487  txcmplem2  23505  hausdiag  23508  txkgen  23515  xkococnlem  23522  qtoptop2  23562  basqtop  23574  fbssfi  23700  filin  23717  infil  23726  fbasrn  23747  fgtr  23753  ufprim  23772  flimrest  23846  txflf  23869  fclsrest  23887  alexsubALTlem4  23913  tsmsres  24007  tsmsxplem1  24016  ustund  24085  trust  24093  utoptop  24098  restutop  24101  cfiluweak  24158  xmetres  24228  metres  24229  blin2  24293  setsmstopn  24342  metrest  24388  ressxms  24389  tgioo  24660  xrsmopn  24677  reconnlem1  24691  xrge0tsms  24699  tcphcph  25113  cfilresi  25171  cfilres  25172  caussi  25173  causs  25174  relcmpcmet  25194  minveclem4a  25306  ismbl2  25404  cmmbl  25411  nulmbl2  25413  unmbl  25414  shftmbl  25415  volinun  25423  voliunlem1  25427  voliunlem2  25428  ioombl1lem4  25438  ioombl1  25439  uniioombllem2  25460  uniioombllem3  25462  uniioombllem4  25463  uniioombllem5  25464  uniioombl  25466  volivth  25484  vitalilem3  25487  vitalilem4  25488  vitalilem5  25489  vitali  25490  mbfadd  25538  mbfsub  25539  i1fadd  25572  itg1addlem2  25574  itg1addlem4  25576  itg1addlem5  25577  itg1climres  25591  mbfmul  25603  itg2splitlem  25625  itg2split  25626  limcresi  25762  limciun  25771  dvreslem  25786  dvres2lem  25787  dvres  25788  dvres3a  25791  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  ig1peu  26056  pilem2  26338  pilem3  26339  rlimcnp2  26852  ppisval  26990  ppifi  26992  ppiprm  27037  chtprm  27039  chtdif  27044  efchtdvds  27045  ppidif  27049  ppiltx  27063  prmorcht  27064  ppiub  27091  chtlepsi  27093  pclogsum  27102  vmasum  27103  chpval2  27105  chpub  27107  2sqlem8  27313  chebbnd1lem1  27356  chtppilimlem1  27360  rpvmasum2  27399  dchrisum0re  27400  rplogsum  27414  dirith2  27415  nosupbnd1lem1  27596  nosupbnd2  27604  noinfbnd1lem1  27611  axtgcgrrflx  28365  axtgcgrid  28366  axtgsegcon  28367  axtg5seg  28368  axtgbtwnid  28369  axtgpasch  28370  axtgcont1  28371  phnv  30716  minvecolem2  30777  minvecolem3  30778  minvecolem5  30783  minvecolem6  30784  minvecolem7  30785  hlimcaui  31138  chdmm1i  31379  chabs1  31418  chabs2  31419  ledii  31438  lejdii  31440  pjoml4i  31489  cmbr3i  31502  cmbr4i  31503  cmm1i  31508  osumcor2i  31546  3oalem4  31567  pjssmii  31583  pjocini  31600  pjini  31601  mayete3i  31630  riesz4  31966  riesz1  31967  cnlnadjeui  31979  cnlnadjeu  31980  cnlnssadj  31982  nmopadjlei  31990  pjin1i  32094  pjclem1  32097  stji1i  32144  stm1i  32145  dmdbr2  32205  ssmd1  32213  mdslj2i  32222  mdsl2bi  32225  mdslmd1lem1  32227  mdslmd2i  32232  atomli  32284  atcvat4i  32299  sumdmdlem2  32321  dmdbr5ati  32324  dmdbr6ati  32325  dmdbr7ati  32326  indifbi  32422  disjxpin  32490  imadifxp  32503  nfpconfp  32529  off2  32538  ffsrn  32625  indsumin  32758  indf1ofs  32762  gsummptres  32965  xrge0tsmsd  32975  idlinsubrg  33375  ordtrestNEW  33884  qqhnm  33953  qqhcn  33954  rrhre  33984  esumval  34009  esumel  34010  gsumesum  34022  esumlub  34023  esumcst  34026  esumfsup  34033  esumpcvgval  34041  esumcvg  34049  sigainb  34099  ldgenpisyslem1  34126  measinb2  34186  sibfinima  34303  sibfof  34304  eulerpartlemelr  34321  eulerpartlem1  34331  eulerpartgbij  34336  eulerpartlemgu  34341  eulerpartlemgs2  34344  sseqf  34356  ballotlemfelz  34455  ballotlemfp1  34456  reprinrn  34582  reprinfz1  34586  hgt750lemd  34612  bnj1292  34778  connpconn  35195  iccllysconn  35210  cvmsss2  35234  cvmcov2  35235  cvmopnlem  35238  cvmliftmolem2  35242  cvmliftlem15  35258  cvmlift2lem12  35274  mvrsfpw  35466  msrf  35502  elmsta  35508  mthmpps  35542  nepss  35678  dfon2lem4  35747  txpss3v  35839  fixssdm  35867  fixssrn  35868  limitssson  35872  fneer  36314  neibastop1  36320  neibastop2lem  36321  filnetlem3  36341  ontopbas  36389  bj-disj2r  36989  bj-restpw  37053  bj-discrmoore  37072  bj-idres  37121  bj-fvsnun2  37217  bj-ablssgrp  37237  bj-fldssdrng  37249  taupilemrplb  37281  taupilem2  37283  taupi  37284  ptrest  37586  poimirlem29  37616  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  mbfposadd  37634  sstotbnd2  37741  ssbnd  37755  heibor1lem  37776  heiborlem1  37778  heiborlem3  37780  heiborlem5  37782  heiborlem6  37783  heiborlem10  37787  heibor  37788  opidonOLD  37819  exidcl  37843  flddivrng  37966  iss2  38299  xrnss3v  38327  refrelsredund2  38597  lshpinN  38955  lcvexchlem5  39004  pmodlem2  39814  pmod1i  39815  pmodN  39817  osumcllem7N  39929  pexmidlem4N  39940  pl42lem3N  39948  djaclN  41103  dihoml4c  41343  dochdmj1  41357  djhcl  41367  dochexmidlem4  41430  mapd1o  41615  mapdin  41629  unitscyglem5  42160  redvmptabs  42321  elrfi  42655  elrfirn  42656  elrfirn2  42657  ismrcd1  42659  istopclsd  42661  isnacs2  42667  mrefg3  42669  isnacs3  42671  diophrw  42720  diophin  42733  aomclem2  43017  islmodfg  43031  lsmfgcl  43036  lmhmfgima  43046  lmhmfgsplit  43048  lmhmlnmsplit  43049  pwfi2f1o  43058  hbt  43092  ofoafg  43316  harval3  43500  elinintrab  43539  trrelind  43627  clsk3nimkb  44002  isotone2  44011  ismnushort  44263  onfrALTlem2  44509  onfrALTlem2VD  44851  wfac8prim  44965  unirestss  45091  inmap  45176  fsumiunss  45546  islptre  45590  sumnnodd  45601  limclner  45622  liminfval4  45760  liminfval3  45761  cnrefiisplem  45800  cncfuni  45857  ismbl3  45957  ismbl4  45964  fouriersw  46202  qndenserrnbllem  46265  salincl  46295  salgencntex  46314  sge0less  46363  sge0resplit  46377  sge0split  46380  sge0iunmptlemre  46386  carageniuncllem1  46492  carageniuncllem2  46493  caragenel2d  46503  hspmbllem3  46599  hspmbl  46600  ovolval2lem  46614  sssmf  46709  smfaddlem1  46734  smflimlem2  46743  smflimlem3  46744  smflimlem4  46745  smfres  46761  smfmullem4  46765  smfsuplem1  46782  fcoreslem2  47038  rngcrescrhmALTV  48241  rhmsubcALTVlem1  48242  funcringcsetcALTV2lem9  48259  fldcALTV  48293  fldhmsubcALTV  48294  iscnrm3llem2  48911  uptrlem1  49172  uptrlem2  49173  uptrlem3  49174  uptra  49177  uptrar  49178  uobeqw  49181  uptr2  49183  uptr2a  49184  fucoppcfunc  49374  setrec2fun  49654