Theorem inss1 4184

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

Syntax hints:   ∩ cin 3896   ⊆ wss 3897

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  inss2  4185  ssinss1  4193  unabs  4212  nssinpss  4214  dfin4  4225  inv1  4345  disjdif  4419  ifssun  4490  uniintsn  4933  wefrc  5608  relin1  5751  resss  5949  resmpt3  5986  cnvcnvss  6141  resdmss  6182  resssxp  6217  predss  6256  ordtri3or  6338  onfr  6345  ordelinel  6409  funin  6557  funimass2  6564  fnresin1  6606  fnres  6608  fresin  6692  fresaun  6694  nfvres  6860  ssimaex  6907  fneqeql2  6980  fnfvimad  7168  funiunfv  7182  isoini2  7273  ofrfvalg  7618  ofval  7621  ofrval  7622  off  7628  ofres  7629  ofco  7635  fparlem3  8044  fparlem4  8045  frrlem4  8219  frrlem13  8228  smores  8272  smores2  8274  tfrlem5  8299  pmresg  8794  sbthlem7  9006  sbthcl  9012  infi  9154  imafi  9199  ixpfi2  9234  unifpw  9239  elfiun  9314  dffi3  9315  marypha1lem  9317  ordtypelem6  9409  ordtypelem7  9410  ordtypelem8  9411  wdomima2g  9472  frmin  9642  frrlem15  9650  frrlem16  9651  tskwe  9843  ackbij1lem15  10124  ackbij1lem16  10125  fin23lem23  10217  fin23lem22  10218  fin23lem19  10227  brdom3  10419  brdom5  10420  brdom4  10421  imadomg  10425  fpwwe2lem11  10532  canthp1lem2  10544  wunin  10604  tskin  10650  gruima  10693  ingru  10706  gruina  10709  grur1a  10710  nqerf  10821  nqerrel  10823  hashun3  14291  hashin  14318  hashdif  14320  xptrrel  14887  rexanuz  15253  limsupgle  15384  rlimres  15465  lo1res  15466  lo1resb  15471  rlimresb  15472  o1resb  15473  lo1eq  15475  rlimeq  15476  o1of2  15520  o1rlimmul  15526  isercolllem2  15573  isercolllem3  15574  isercoll  15575  incexclem  15743  incexc  15744  bitsinvp1  16360  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadaddlem  16377  sadasslem  16381  sadeq  16383  bitsres  16384  smuval2  16393  smupval  16399  smueqlem  16401  smumul  16404  ramub2  16926  ramub1lem2  16939  fvsetsid  17079  ressbasss2  17152  ressinbas  17156  ressress  17158  submre  17507  isacs1i  17563  mreacs  17564  acsfn  17565  invss  17668  sscres  17730  catcisolem  18017  catciso  18018  isacs5lem  18451  psss  18486  tsrss  18495  tsrdir  18510  sylow2a  19531  lsmmod  19587  gsumzres  19821  gsumzaddlem  19833  dprddisj2  19953  ablfac1eu  19987  isunit  20291  rngcbas  20536  rngchomfval  20537  rngccofval  20541  dfrngc2  20543  rnghmsscmap2  20544  rnghmsscmap  20545  rngcsect  20551  funcrngcsetc  20555  ringcbas  20565  ringchomfval  20566  ringccofval  20570  dfringc2  20572  rhmsscmap2  20573  rhmsscmap  20574  rhmsscrnghm  20580  ringcsect  20585  funcringcsetc  20589  rngcrescrhm  20599  rhmsubclem1  20600  fldc  20699  fldhmsubc  20700  acsfn1p  20714  lspextmo  20990  2idlval  21188  pjfval  21643  pjpm  21645  aspsubrg  21813  psrbagsn  21998  ofco2  22366  basdif0  22868  tgval2  22871  eltg3  22877  tgcl  22884  tgdom  22893  tgidm  22895  ppttop  22922  epttop  22924  ntropn  22964  ntrin  22976  mretopd  23007  neiptoptop  23046  restfpw  23094  neitr  23095  restcls  23096  cncls  23189  cnpresti  23203  cnprest  23204  cmpsublem  23314  cmpsub  23315  fiuncmp  23319  indisconn  23333  connsub  23336  iunconnlem  23342  islly2  23399  cldllycmp  23410  kgentopon  23453  ptbasfi  23496  ptcnplem  23536  txcnmpt  23539  txcmplem2  23557  hausdiag  23560  txkgen  23567  xkococnlem  23574  qtoptop2  23614  basqtop  23626  fbssfi  23752  filin  23769  infil  23778  fbasrn  23799  fgtr  23805  ufprim  23824  flimrest  23898  txflf  23921  fclsrest  23939  alexsubALTlem4  23965  tsmsres  24059  tsmsxplem1  24068  ustund  24137  trust  24144  utoptop  24149  restutop  24152  cfiluweak  24209  xmetres  24279  metres  24280  blin2  24344  setsmstopn  24393  metrest  24439  ressxms  24440  tgioo  24711  xrsmopn  24728  reconnlem1  24742  xrge0tsms  24750  tcphcph  25164  cfilresi  25222  cfilres  25223  caussi  25224  causs  25225  relcmpcmet  25245  minveclem4a  25357  ismbl2  25455  cmmbl  25462  nulmbl2  25464  unmbl  25465  shftmbl  25466  volinun  25474  voliunlem1  25478  voliunlem2  25479  ioombl1lem4  25489  ioombl1  25490  uniioombllem2  25511  uniioombllem3  25513  uniioombllem4  25514  uniioombllem5  25515  uniioombl  25517  volivth  25535  vitalilem3  25538  vitalilem4  25539  vitalilem5  25540  vitali  25541  mbfadd  25589  mbfsub  25590  i1fadd  25623  itg1addlem2  25625  itg1addlem4  25627  itg1addlem5  25628  itg1climres  25642  mbfmul  25654  itg2splitlem  25676  itg2split  25677  limcresi  25813  limciun  25822  dvreslem  25837  dvres2lem  25838  dvres  25839  dvres3a  25842  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  ig1peu  26107  pilem2  26389  pilem3  26390  rlimcnp2  26903  ppisval  27041  ppifi  27043  ppiprm  27088  chtprm  27090  chtdif  27095  efchtdvds  27096  ppidif  27100  ppiltx  27114  prmorcht  27115  ppiub  27142  chtlepsi  27144  pclogsum  27153  vmasum  27154  chpval2  27156  chpub  27158  2sqlem8  27364  chebbnd1lem1  27407  chtppilimlem1  27411  rpvmasum2  27450  dchrisum0re  27451  rplogsum  27465  dirith2  27466  nosupbnd1lem1  27647  nosupbnd2  27655  noinfbnd1lem1  27662  axtgcgrrflx  28440  axtgcgrid  28441  axtgsegcon  28442  axtg5seg  28443  axtgbtwnid  28444  axtgpasch  28445  axtgcont1  28446  phnv  30794  minvecolem2  30855  minvecolem3  30856  minvecolem5  30861  minvecolem6  30862  minvecolem7  30863  hlimcaui  31216  chdmm1i  31457  chabs1  31496  chabs2  31497  ledii  31516  lejdii  31518  pjoml4i  31567  cmbr3i  31580  cmbr4i  31581  cmm1i  31586  osumcor2i  31624  3oalem4  31645  pjssmii  31661  pjocini  31678  pjini  31679  mayete3i  31708  riesz4  32044  riesz1  32045  cnlnadjeui  32057  cnlnadjeu  32058  cnlnssadj  32060  nmopadjlei  32068  pjin1i  32172  pjclem1  32175  stji1i  32222  stm1i  32223  dmdbr2  32283  ssmd1  32291  mdslj2i  32300  mdsl2bi  32303  mdslmd1lem1  32305  mdslmd2i  32310  atomli  32362  atcvat4i  32377  sumdmdlem2  32399  dmdbr5ati  32402  dmdbr6ati  32403  dmdbr7ati  32404  indifbi  32500  disjxpin  32568  imadifxp  32581  nfpconfp  32614  off2  32623  ffsrn  32711  indsumin  32843  indf1ofs  32847  gsummptres  33032  xrge0tsmsd  33042  idlinsubrg  33396  ordtrestNEW  33934  qqhnm  34003  qqhcn  34004  rrhre  34034  esumval  34059  esumel  34060  gsumesum  34072  esumlub  34073  esumcst  34076  esumfsup  34083  esumpcvgval  34091  esumcvg  34099  sigainb  34149  ldgenpisyslem1  34176  measinb2  34236  sibfinima  34352  sibfof  34353  eulerpartlemelr  34370  eulerpartlem1  34380  eulerpartgbij  34385  eulerpartlemgu  34390  eulerpartlemgs2  34393  sseqf  34405  ballotlemfelz  34504  ballotlemfp1  34505  reprinrn  34631  reprinfz1  34635  hgt750lemd  34661  bnj1292  34827  connpconn  35279  iccllysconn  35294  cvmsss2  35318  cvmcov2  35319  cvmopnlem  35322  cvmliftmolem2  35326  cvmliftlem15  35342  cvmlift2lem12  35358  mvrsfpw  35550  msrf  35586  elmsta  35592  mthmpps  35626  nepss  35762  dfon2lem4  35828  txpss3v  35920  fixssdm  35948  fixssrn  35949  limitssson  35953  fneer  36397  neibastop1  36403  neibastop2lem  36404  filnetlem3  36424  ontopbas  36472  bj-disj2r  37072  bj-restpw  37136  bj-discrmoore  37155  bj-idres  37204  bj-fvsnun2  37300  bj-ablssgrp  37320  bj-fldssdrng  37332  taupilemrplb  37364  taupilem2  37366  taupi  37367  ptrest  37669  poimirlem29  37699  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  mbfposadd  37717  sstotbnd2  37824  ssbnd  37838  heibor1lem  37859  heiborlem1  37861  heiborlem3  37863  heiborlem5  37865  heiborlem6  37866  heiborlem10  37870  heibor  37871  opidonOLD  37902  exidcl  37926  flddivrng  38049  iss2  38386  xrnss3v  38415  refrelsredund2  38739  lshpinN  39098  lcvexchlem5  39147  pmodlem2  39956  pmod1i  39957  pmodN  39959  osumcllem7N  40071  pexmidlem4N  40082  pl42lem3N  40090  djaclN  41245  dihoml4c  41485  dochdmj1  41499  djhcl  41509  dochexmidlem4  41572  mapd1o  41757  mapdin  41771  unitscyglem5  42302  redvmptabs  42463  elrfi  42797  elrfirn  42798  elrfirn2  42799  ismrcd1  42801  istopclsd  42803  isnacs2  42809  mrefg3  42811  isnacs3  42813  diophrw  42862  diophin  42875  aomclem2  43158  islmodfg  43172  lsmfgcl  43177  lmhmfgima  43187  lmhmfgsplit  43189  lmhmlnmsplit  43190  pwfi2f1o  43199  hbt  43233  ofoafg  43457  harval3  43641  elinintrab  43680  trrelind  43768  clsk3nimkb  44143  isotone2  44152  ismnushort  44404  onfrALTlem2  44649  onfrALTlem2VD  44991  wfac8prim  45105  unirestss  45231  inmap  45316  fsumiunss  45685  islptre  45729  sumnnodd  45740  limclner  45759  liminfval4  45897  liminfval3  45898  cnrefiisplem  45937  cncfuni  45994  ismbl3  46094  ismbl4  46101  fouriersw  46339  qndenserrnbllem  46402  salincl  46432  salgencntex  46451  sge0less  46500  sge0resplit  46514  sge0split  46517  sge0iunmptlemre  46523  carageniuncllem1  46629  carageniuncllem2  46630  caragenel2d  46640  hspmbllem3  46736  hspmbl  46737  ovolval2lem  46751  sssmf  46846  smfaddlem1  46871  smflimlem2  46880  smflimlem3  46881  smflimlem4  46882  smfres  46898  smfmullem4  46902  smfsuplem1  46919  fcoreslem2  47174  rngcrescrhmALTV  48390  rhmsubcALTVlem1  48391  funcringcsetcALTV2lem9  48408  fldcALTV  48442  fldhmsubcALTV  48443  iscnrm3llem2  49060  uptrlem1  49321  uptrlem2  49322  uptrlem3  49323  uptra  49326  uptrar  49327  uobeqw  49330  uptr2  49332  uptr2a  49333  fucoppcfunc  49523  setrec2fun  49803