Theorem inss1 4177

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

Syntax hints:   ∩ cin 3888   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  inss2  4178  ssinss1  4186  unabs  4205  nssinpss  4207  dfin4  4218  inv1  4338  disjdif  4412  ifssun  4484  uniintsn  4927  wefrc  5625  relin1  5768  resss  5966  resmpt3  6003  cnvcnvss  6158  resdmss  6199  resssxp  6234  predss  6273  ordtri3or  6355  onfr  6362  ordelinel  6426  funin  6574  funimass2  6581  fnresin1  6623  fnres  6625  fresin  6709  fresaun  6711  nfvres  6878  ssimaex  6925  fneqeql2  6999  fnfvimad  7189  funiunfv  7203  isoini2  7294  ofrfvalg  7639  ofval  7642  ofrval  7643  off  7649  ofres  7650  ofco  7656  fparlem3  8064  fparlem4  8065  frrlem4  8239  frrlem13  8248  smores  8292  smores2  8294  tfrlem5  8319  pmresg  8818  sbthlem7  9031  sbthcl  9037  infi  9180  imafi  9225  ixpfi2  9260  unifpw  9265  elfiun  9343  dffi3  9344  marypha1lem  9346  ordtypelem6  9438  ordtypelem7  9439  ordtypelem8  9440  wdomima2g  9501  frmin  9673  frrlem15  9681  frrlem16  9682  tskwe  9874  ackbij1lem15  10155  ackbij1lem16  10156  fin23lem23  10248  fin23lem22  10249  fin23lem19  10258  brdom3  10450  brdom5  10451  brdom4  10452  imadomg  10456  fpwwe2lem11  10564  canthp1lem2  10576  wunin  10636  tskin  10682  gruima  10725  ingru  10738  gruina  10741  grur1a  10742  nqerf  10853  nqerrel  10855  hashun3  14346  hashin  14373  hashdif  14375  xptrrel  14942  rexanuz  15308  limsupgle  15439  rlimres  15520  lo1res  15521  lo1resb  15526  rlimresb  15527  o1resb  15528  lo1eq  15530  rlimeq  15531  o1of2  15575  o1rlimmul  15581  isercolllem2  15628  isercolllem3  15629  isercoll  15630  incexclem  15801  incexc  15802  bitsinvp1  16418  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  sadeq  16441  bitsres  16442  smuval2  16451  smupval  16457  smueqlem  16459  smumul  16462  ramub2  16985  ramub1lem2  16998  fvsetsid  17138  ressbasss2  17211  ressinbas  17215  ressress  17217  submre  17567  isacs1i  17623  mreacs  17624  acsfn  17625  invss  17728  sscres  17790  catcisolem  18077  catciso  18078  isacs5lem  18511  psss  18546  tsrss  18555  tsrdir  18570  sylow2a  19594  lsmmod  19650  gsumzres  19884  gsumzaddlem  19896  dprddisj2  20016  ablfac1eu  20050  isunit  20353  rngcbas  20598  rngchomfval  20599  rngccofval  20603  dfrngc2  20605  rnghmsscmap2  20606  rnghmsscmap  20607  rngcsect  20613  funcrngcsetc  20617  ringcbas  20627  ringchomfval  20628  ringccofval  20632  dfringc2  20634  rhmsscmap2  20635  rhmsscmap  20636  rhmsscrnghm  20642  ringcsect  20647  funcringcsetc  20651  rngcrescrhm  20661  rhmsubclem1  20662  fldc  20761  fldhmsubc  20762  acsfn1p  20776  lspextmo  21051  2idlval  21249  pjfval  21686  pjpm  21688  aspsubrg  21855  psrbagsn  22041  ofco2  22416  basdif0  22918  tgval2  22921  eltg3  22927  tgcl  22934  tgdom  22943  tgidm  22945  ppttop  22972  epttop  22974  ntropn  23014  ntrin  23026  mretopd  23057  neiptoptop  23096  restfpw  23144  neitr  23145  restcls  23146  cncls  23239  cnpresti  23253  cnprest  23254  cmpsublem  23364  cmpsub  23365  fiuncmp  23369  indisconn  23383  connsub  23386  iunconnlem  23392  islly2  23449  cldllycmp  23460  kgentopon  23503  ptbasfi  23546  ptcnplem  23586  txcnmpt  23589  txcmplem2  23607  hausdiag  23610  txkgen  23617  xkococnlem  23624  qtoptop2  23664  basqtop  23676  fbssfi  23802  filin  23819  infil  23828  fbasrn  23849  fgtr  23855  ufprim  23874  flimrest  23948  txflf  23971  fclsrest  23989  alexsubALTlem4  24015  tsmsres  24109  tsmsxplem1  24118  ustund  24187  trust  24194  utoptop  24199  restutop  24202  cfiluweak  24259  xmetres  24329  metres  24330  blin2  24394  setsmstopn  24443  metrest  24489  ressxms  24490  tgioo  24761  xrsmopn  24778  reconnlem1  24792  xrge0tsms  24800  tcphcph  25204  cfilresi  25262  cfilres  25263  caussi  25264  causs  25265  relcmpcmet  25285  minveclem4a  25397  ismbl2  25494  cmmbl  25501  nulmbl2  25503  unmbl  25504  shftmbl  25505  volinun  25513  voliunlem1  25517  voliunlem2  25518  ioombl1lem4  25528  ioombl1  25529  uniioombllem2  25550  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombl  25556  volivth  25574  vitalilem3  25577  vitalilem4  25578  vitalilem5  25579  vitali  25580  mbfadd  25628  mbfsub  25629  i1fadd  25662  itg1addlem2  25664  itg1addlem4  25666  itg1addlem5  25667  itg1climres  25681  mbfmul  25693  itg2splitlem  25715  itg2split  25716  limcresi  25852  limciun  25861  dvreslem  25876  dvres2lem  25877  dvres  25878  dvres3a  25881  dvaddbr  25905  dvmulbr  25906  dvfsumle  25988  dvfsumabs  25990  ig1peu  26140  pilem2  26417  pilem3  26418  rlimcnp2  26930  ppisval  27067  ppifi  27069  ppiprm  27114  chtprm  27116  chtdif  27121  efchtdvds  27122  ppidif  27126  ppiltx  27140  prmorcht  27141  ppiub  27167  chtlepsi  27169  pclogsum  27178  vmasum  27179  chpval2  27181  chpub  27183  2sqlem8  27389  chebbnd1lem1  27432  chtppilimlem1  27436  rpvmasum2  27475  dchrisum0re  27476  rplogsum  27490  dirith2  27491  nosupbnd1lem1  27672  nosupbnd2  27680  noinfbnd1lem1  27687  axtgcgrrflx  28530  axtgcgrid  28531  axtgsegcon  28532  axtg5seg  28533  axtgbtwnid  28534  axtgpasch  28535  axtgcont1  28536  phnv  30885  minvecolem2  30946  minvecolem3  30947  minvecolem5  30952  minvecolem6  30953  minvecolem7  30954  hlimcaui  31307  chdmm1i  31548  chabs1  31587  chabs2  31588  ledii  31607  lejdii  31609  pjoml4i  31658  cmbr3i  31671  cmbr4i  31672  cmm1i  31677  osumcor2i  31715  3oalem4  31736  pjssmii  31752  pjocini  31769  pjini  31770  mayete3i  31799  riesz4  32135  riesz1  32136  cnlnadjeui  32148  cnlnadjeu  32149  cnlnssadj  32151  nmopadjlei  32159  pjin1i  32263  pjclem1  32266  stji1i  32313  stm1i  32314  dmdbr2  32374  ssmd1  32382  mdslj2i  32391  mdsl2bi  32394  mdslmd1lem1  32396  mdslmd2i  32401  atomli  32453  atcvat4i  32468  sumdmdlem2  32490  dmdbr5ati  32493  dmdbr6ati  32494  dmdbr7ati  32495  indifbi  32590  disjxpin  32658  imadifxp  32671  nfpconfp  32705  off2  32714  ffsrn  32801  indsumin  32921  indf1ofs  32926  gsummptres  33113  xrge0tsmsd  33134  idlinsubrg  33491  ordtrestNEW  34065  qqhnm  34134  qqhcn  34135  rrhre  34165  esumval  34190  esumel  34191  gsumesum  34203  esumlub  34204  esumcst  34207  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  sigainb  34280  ldgenpisyslem1  34307  measinb2  34367  sibfinima  34483  sibfof  34484  eulerpartlemelr  34501  eulerpartlem1  34511  eulerpartgbij  34516  eulerpartlemgu  34521  eulerpartlemgs2  34524  sseqf  34536  ballotlemfelz  34635  ballotlemfp1  34636  reprinrn  34762  reprinfz1  34766  hgt750lemd  34792  bnj1292  34957  connpconn  35417  iccllysconn  35432  cvmsss2  35456  cvmcov2  35457  cvmopnlem  35460  cvmliftmolem2  35464  cvmliftlem15  35480  cvmlift2lem12  35496  mvrsfpw  35688  msrf  35724  elmsta  35730  mthmpps  35764  nepss  35900  dfon2lem4  35966  txpss3v  36058  fixssdm  36086  fixssrn  36087  limitssson  36091  fneer  36535  neibastop1  36541  neibastop2lem  36542  filnetlem3  36562  ontopbas  36610  bj-disj2r  37335  bj-restpw  37404  bj-discrmoore  37423  bj-idres  37474  bj-fvsnun2  37570  bj-ablssgrp  37590  bj-fldssdrng  37602  taupilemrplb  37634  taupilem2  37636  taupi  37637  ptrest  37940  poimirlem29  37970  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  mbfposadd  37988  sstotbnd2  38095  ssbnd  38109  heibor1lem  38130  heiborlem1  38132  heiborlem3  38134  heiborlem5  38136  heiborlem6  38137  heiborlem10  38141  heibor  38142  opidonOLD  38173  exidcl  38197  flddivrng  38320  iss2  38665  xrnss3v  38702  refrelsredund2  39038  lshpinN  39435  lcvexchlem5  39484  pmodlem2  40293  pmod1i  40294  pmodN  40296  osumcllem7N  40408  pexmidlem4N  40419  pl42lem3N  40427  djaclN  41582  dihoml4c  41822  dochdmj1  41836  djhcl  41846  dochexmidlem4  41909  mapd1o  42094  mapdin  42108  unitscyglem5  42638  redvmptabs  42792  elrfi  43126  elrfirn  43127  elrfirn2  43128  ismrcd1  43130  istopclsd  43132  isnacs2  43138  mrefg3  43140  isnacs3  43142  diophrw  43191  diophin  43204  aomclem2  43483  islmodfg  43497  lsmfgcl  43502  lmhmfgima  43512  lmhmfgsplit  43514  lmhmlnmsplit  43515  pwfi2f1o  43524  hbt  43558  ofoafg  43782  harval3  43965  elinintrab  44004  trrelind  44092  clsk3nimkb  44467  isotone2  44476  ismnushort  44728  onfrALTlem2  44973  onfrALTlem2VD  45315  wfac8prim  45429  unirestss  45554  inmap  45638  fsumiunss  46005  islptre  46049  sumnnodd  46060  limclner  46079  liminfval4  46217  liminfval3  46218  cnrefiisplem  46257  cncfuni  46314  ismbl3  46414  ismbl4  46421  fouriersw  46659  qndenserrnbllem  46722  salincl  46752  salgencntex  46771  sge0less  46820  sge0resplit  46834  sge0split  46837  sge0iunmptlemre  46843  carageniuncllem1  46949  carageniuncllem2  46950  caragenel2d  46960  hspmbllem3  47056  hspmbl  47057  ovolval2lem  47071  sssmf  47166  smfaddlem1  47191  smflimlem2  47200  smflimlem3  47201  smflimlem4  47202  smfres  47218  smfmullem4  47222  smfsuplem1  47239  fcoreslem2  47512  indprmfz  48093  ppivalnn  48095  rngcrescrhmALTV  48756  rhmsubcALTVlem1  48757  funcringcsetcALTV2lem9  48774  fldcALTV  48808  fldhmsubcALTV  48809  iscnrm3llem2  49425  uptrlem1  49685  uptrlem2  49686  uptrlem3  49687  uptra  49690  uptrar  49691  uobeqw  49694  uptr2  49696  uptr2a  49697  fucoppcfunc  49887  setrec2fun  50167