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

This proof depends on syntax axioms:   ∩ cin 3905   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ss 3923

This theorem is used by:  inss2  4190  ssinss1  4198  ssinss1OLD  4199  unabs  4218  nssinpss  4220  dfin4  4231  inv1  4355  vvin  4366  ifssun  4507  uniin  4898  uniintsn  4952  wefrc  5657  relin1  5801  resss  6002  resindm  6031  resmpt3  6042  rnin  6145  cnvcnvssOLD  6195  resdmss  6238  resssxp  6274  predss  6314  ordtri3or  6397  onfr  6404  ordelinel  6468  funin  6616  funimass2  6623  fnresin1  6664  fnres  6666  fresin  6751  fresaun  6753  nfvres  6923  ssimaex  6970  fneqeql2  7046  fnfvimad  7239  funiunfv  7251  isoini2  7346  ofrfvalg  7692  ofval  7695  ofrval  7696  off  7702  ofres  7703  ofco  7709  fparlem3  8115  fparlem4  8116  frrlem4  8292  frrlem13  8301  smores  8345  smores2  8347  tfrlem5  8372  pmresg  8874  sbthlem7  9088  sbthcl  9094  infi  9237  imafi  9282  ixpfi2  9314  unifpw  9319  elfiun  9397  dffi3  9398  marypha1lem  9400  ordtypelem6  9492  ordtypelem7  9493  ordtypelem8  9494  wdomima2g  9555  frmin  9728  frrlem15  9736  frrlem16  9737  tskwe  9952  ackbij1lem15  10232  ackbij1lem16  10233  fin23lem23  10325  fin23lem22  10326  fin23lem19  10335  brdom3  10527  brdom5  10528  brdom4  10529  imadomg  10533  fpwwe2lem11  10643  canthp1lem2  10655  wunin  10715  tskin  10761  gruima  10804  ingru  10817  gruina  10820  grur1a  10821  nqerf  10932  nqerrel  10934  hashun3  14440  hashin  14468  hashdif  14470  xptrrel  15043  rexanuz  15423  limsupgle  15554  rlimres  15635  lo1res  15636  lo1resb  15641  rlimresb  15642  o1resb  15643  lo1eq  15645  rlimeq  15646  o1of2  15690  o1rlimmul  15696  isercolllem2  15743  isercolllem3  15744  isercoll  15745  incexclem  15915  incexc  15916  bitsinvp1  16531  sadcaddlem  16539  sadadd2lem  16541  sadadd3  16543  sadaddlem  16548  sadasslem  16552  sadeq  16554  bitsres  16555  smuval2  16564  smupval  16570  smueqlem  16572  smumul  16575  ramub2  17098  ramub1lem2  17111  fvsetsid  17252  ressbasss2  17325  ressinbas  17329  ressress  17331  submre  17681  isacs1i  17737  mreacs  17738  acsfn  17739  invss  17842  sscres  17904  catcisolem  18191  catciso  18192  isacs5lem  18625  psss  18660  tsrss  18669  tsrdir  18684  sylow2a  19735  lsmmod  19791  gsumzres  20025  gsumzaddlem  20037  dprddisj2  20157  ablfac1eu  20191  isunit  20503  rngcbas  20772  rngchomfval  20773  rngccofval  20777  dfrngc2  20779  rnghmsscmap2  20780  rnghmsscmap  20781  rngcsect  20787  funcrngcsetc  20791  ringcbas  20801  ringchomfval  20802  ringccofval  20806  dfringc2  20808  rhmsscmap2  20809  rhmsscmap  20810  rhmsscrnghm  20816  ringcsect  20821  funcringcsetc  20825  rngcrescrhm  20835  rhmsubclem1  20836  fldc  20939  fldhmsubc  20940  acsfn1p  20954  lspextmo  21229  2idlval  21442  pjfval  21908  pjpm  21910  aspsubrg  22077  psrbagsn  22266  ofco2  22660  basdif0  23162  tgval2  23165  eltg3  23171  tgcl  23178  tgdom  23187  tgidm  23189  ppttop  23216  epttop  23218  ntropn  23258  ntrin  23270  mretopd  23301  neiptoptop  23340  restfpw  23388  neitr  23389  restcls  23390  cncls  23483  cnpresti  23497  cnprest  23498  cmpsublem  23608  cmpsub  23609  fiuncmp  23613  indisconn  23627  connsub  23630  iunconnlem  23636  islly2  23694  cldllycmp  23705  kgentopon  23748  ptbasfi  23791  ptcnplem  23831  txcnmpt  23834  txcmplem2  23852  hausdiag  23855  txkgen  23862  xkococnlem  23869  qtoptop2  23909  basqtop  23921  fbssfi  24047  filin  24064  infil  24073  fbasrn  24094  fgtr  24100  ufprim  24119  flimrest  24193  txflf  24216  fclsrest  24234  alexsubALTlem4  24260  tsmsres  24354  tsmsxplem1  24363  ustund  24432  trust  24439  utoptop  24444  restutop  24447  cfiluweak  24504  xmetres  24574  metres  24575  blin2  24639  setsmstopn  24688  metrest  24734  ressxms  24735  tgioo  25006  xrsmopn  25023  reconnlem1  25037  xrge0tsms  25045  tcphcph  25449  cfilresi  25507  cfilres  25508  caussi  25509  causs  25510  relcmpcmet  25530  minveclem4a  25642  ismbl2  25739  cmmbl  25746  nulmbl2  25748  unmbl  25749  shftmbl  25750  volinun  25758  voliunlem1  25762  voliunlem2  25763  ioombl1lem4  25773  ioombl1  25774  uniioombllem2  25795  uniioombllem3  25797  uniioombllem4  25798  uniioombllem5  25799  uniioombl  25801  volivth  25819  vitalilem3  25822  vitalilem4  25823  vitalilem5  25824  vitali  25825  mbfadd  25873  mbfsub  25874  i1fadd  25907  itg1addlem2  25909  itg1addlem4  25911  itg1addlem5  25912  itg1climres  25926  mbfmul  25938  itg2splitlem  25960  itg2split  25961  limcresi  26097  limciun  26106  dvreslem  26121  dvres2lem  26122  dvres  26123  dvres3a  26126  dvaddbr  26150  dvmulbr  26151  dvfsumle  26233  dvfsumabs  26235  ig1peu  26385  pilem2  26668  pilem3  26669  rlimcnp2  27184  ppisval  27321  ppifi  27323  ppiprm  27368  chtprm  27370  chtdif  27375  efchtdvds  27376  ppidif  27380  ppiltx  27394  prmorcht  27395  ppiub  27421  chtlepsi  27423  pclogsum  27432  vmasum  27433  chpval2  27435  chpub  27437  2sqlem8  27643  chebbnd1lem1  27686  chtppilimlem1  27690  rpvmasum2  27729  dchrisum0re  27730  rplogsum  27744  dirith2  27745  nosupbnd1lem1  27925  nosupbnd2  27933  noinfbnd1lem1  27940  axtgcgrrflx  28784  axtgcgrid  28785  axtgsegcon  28786  axtg5seg  28787  axtgbtwnid  28788  axtgpasch  28789  axtgcont1  28790  phnv  31239  minvecolem2  31300  minvecolem3  31301  minvecolem5  31306  minvecolem6  31307  minvecolem7  31308  hlimcaui  31661  chdmm1i  31902  chabs1  31941  chabs2  31942  ledii  31961  lejdii  31963  pjoml4i  32012  cmbr3i  32025  cmbr4i  32026  cmm1i  32031  osumcor2i  32069  3oalem4  32090  pjssmii  32106  pjocini  32123  pjini  32124  mayete3i  32153  riesz4  32489  riesz1  32490  cnlnadjeui  32502  cnlnadjeu  32503  cnlnssadj  32505  nmopadjlei  32513  pjin1i  32617  pjclem1  32620  stji1i  32667  stm1i  32668  dmdbr2  32728  ssmd1  32736  mdslj2i  32745  mdsl2bi  32748  mdslmd1lem1  32750  mdslmd2i  32755  atomli  32807  atcvat4i  32822  sumdmdlem2  32844  dmdbr5ati  32847  dmdbr6ati  32848  dmdbr7ati  32849  indifbi  32939  disjxpin  33006  imadifxp  33019  nfpconfp  33050  off2  33059  ffsrn  33145  indsumin  33253  indf1ofs  33258  gsummptres  33438  xrge0tsmsd  33459  idlinsubrg  33805  ordtrestNEW  34377  qqhnm  34446  qqhcn  34447  rrhre  34477  esumval  34502  esumel  34503  gsumesum  34515  esumlub  34516  esumcst  34519  esumfsup  34526  esumpcvgval  34534  esumcvg  34542  sigainb  34593  ldgenpisyslem1  34620  measinb2  34680  sibfinima  34796  sibfof  34797  eulerpartlemelr  34814  eulerpartlem1  34824  eulerpartgbij  34829  eulerpartlemgu  34834  eulerpartlemgs2  34837  sseqf  34849  ballotlemfelz  34948  ballotlemfp1  34949  reprinrn  35072  reprinfz1  35076  hgt750lemd  35102  bnj1292  35270  connpconn  35766  iccllysconn  35781  cvmsss2  35805  cvmcov2  35806  cvmopnlem  35809  cvmliftmolem2  35813  cvmliftlem15  35829  cvmlift2lem12  35845  mvrsfpw  36037  msrf  36073  elmsta  36079  mthmpps  36113  nepss  36249  dfon2lem4  36315  txpss3v  36407  fixssdm  36435  fixssrn  36436  limitssson  36440  fneer  36923  neibastop1  36929  neibastop2lem  36930  filnetlem3  36950  ontopbas  36998  bj-disj2r  37723  bj-restpw  37793  bj-discrmoore  37812  bj-idres  37863  bj-fvsnun2  37959  bj-ablssgrp  37979  bj-fldssdrng  37991  taupilemrplb  38023  taupilem2  38025  taupi  38026  ptrest  38329  poimirlem29  38359  mblfinlem3  38369  mblfinlem4  38370  ismblfin  38371  mbfposadd  38377  sstotbnd2  38485  ssbnd  38499  heibor1lem  38520  heiborlem1  38522  heiborlem3  38524  heiborlem5  38526  heiborlem6  38527  heiborlem10  38531  heibor  38532  opidonOLD  38563  exidcl  38587  flddivrng  38710  iss2  39053  xrnss3v  39090  refrelsredund2  39426  lshpinN  39823  lcvexchlem5  39872  pmodlem2  40681  pmod1i  40682  pmodN  40684  osumcllem7N  40796  pexmidlem4N  40807  pl42lem3N  40815  djaclN  41970  dihoml4c  42210  dochdmj1  42224  djhcl  42234  dochexmidlem4  42297  mapd1o  42482  mapdin  42496  unitscyglem5  43026  redvmptabs  43181  elrfi  43485  elrfirn  43486  elrfirn2  43487  ismrcd1  43489  istopclsd  43491  isnacs2  43497  mrefg3  43499  isnacs3  43501  diophrw  43550  diophin  43563  aomclem2  43842  islmodfg  43856  lsmfgcl  43861  lmhmfgima  43871  lmhmfgsplit  43873  lmhmlnmsplit  43874  pwfi2f1o  43883  hbt  43917  ofoafg  44141  harval3  44324  elinintrab  44363  trrelind  44451  clsk3nimkb  44826  isotone2  44835  ismnushort  45071  onfrALTlem2  45315  onfrALTlem2VD  45657  wfac8prim  45771  unirestss  45902  inmap  45985  fsumiunss  46351  islptre  46395  sumnnodd  46406  limclner  46425  liminfval4  46563  liminfval3  46564  cnrefiisplem  46603  cncfuni  46660  ismbl3  46760  ismbl4  46767  fouriersw  47005  qndenserrnbllem  47068  salincl  47098  salgencntex  47117  sge0less  47166  sge0resplit  47180  sge0split  47183  sge0iunmptlemre  47189  carageniuncllem1  47295  carageniuncllem2  47296  caragenel2d  47306  hspmbllem3  47402  hspmbl  47403  ovolval2lem  47417  sssmf  47512  smfaddlem1  47537  smflimlem2  47546  smflimlem3  47547  smflimlem4  47548  smfres  47564  smfmullem4  47568  smfsuplem1  47585  fcoreslem2  47861  indprmfz  48442  ppivalnn  48444  rngcrescrhmALTV  49104  rhmsubcALTVlem1  49105  funcringcsetcALTV2lem9  49122  fldcALTV  49156  fldhmsubcALTV  49157  iscnrm3llem2  49787  uptrlem1  50047  uptrlem2  50048  uptrlem3  50049  uptra  50052  uptrar  50053  uobeqw  50056  uptr2  50058  uptr2a  50059  fucoppcfunc  50249  setrec2fun  50529