Theorem inss1 4165

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

Syntax hints:   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900

This theorem is referenced by:  inss2  4166  ssinss1  4174  unabs  4193  nssinpss  4195  dfin4  4206  inv1  4326  disjdif  4400  ifssun  4472  uniintsn  4915  wefrc  5612  relin1  5755  resss  5953  resmpt3  5990  cnvcnvss  6145  resdmss  6186  resssxp  6221  predss  6260  ordtri3or  6342  onfr  6349  ordelinel  6413  funin  6561  funimass2  6568  fnresin1  6610  fnres  6612  fresin  6696  fresaun  6698  nfvres  6865  ssimaex  6912  fneqeql2  6988  fnfvimad  7178  funiunfv  7192  isoini2  7283  ofrfvalg  7628  ofval  7631  ofrval  7632  off  7638  ofres  7639  ofco  7645  fparlem3  8053  fparlem4  8054  frrlem4  8229  frrlem13  8238  smores  8282  smores2  8284  tfrlem5  8309  pmresg  8808  sbthlem7  9021  sbthcl  9027  infi  9170  imafi  9215  ixpfi2  9250  unifpw  9255  elfiun  9333  dffi3  9334  marypha1lem  9336  ordtypelem6  9428  ordtypelem7  9429  ordtypelem8  9430  wdomima2g  9491  frmin  9664  frrlem15  9672  frrlem16  9673  tskwe  9865  ackbij1lem15  10146  ackbij1lem16  10147  fin23lem23  10239  fin23lem22  10240  fin23lem19  10249  brdom3  10441  brdom5  10442  brdom4  10443  imadomg  10447  fpwwe2lem11  10555  canthp1lem2  10567  wunin  10627  tskin  10673  gruima  10716  ingru  10729  gruina  10732  grur1a  10733  nqerf  10844  nqerrel  10846  hashun3  14337  hashin  14364  hashdif  14366  xptrrel  14933  rexanuz  15299  limsupgle  15430  rlimres  15511  lo1res  15512  lo1resb  15517  rlimresb  15518  o1resb  15519  lo1eq  15521  rlimeq  15522  o1of2  15566  o1rlimmul  15572  isercolllem2  15619  isercolllem3  15620  isercoll  15621  incexclem  15792  incexc  15793  bitsinvp1  16409  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  bitsres  16433  smuval2  16442  smupval  16448  smueqlem  16450  smumul  16453  ramub2  16976  ramub1lem2  16989  fvsetsid  17129  ressbasss2  17202  ressinbas  17206  ressress  17208  submre  17558  isacs1i  17614  mreacs  17615  acsfn  17616  invss  17719  sscres  17781  catcisolem  18068  catciso  18069  isacs5lem  18502  psss  18537  tsrss  18546  tsrdir  18561  sylow2a  19585  lsmmod  19641  gsumzres  19875  gsumzaddlem  19887  dprddisj2  20007  ablfac1eu  20041  isunit  20344  rngcbas  20593  rngchomfval  20594  rngccofval  20598  dfrngc2  20600  rnghmsscmap2  20601  rnghmsscmap  20602  rngcsect  20608  funcrngcsetc  20612  ringcbas  20622  ringchomfval  20623  ringccofval  20627  dfringc2  20629  rhmsscmap2  20630  rhmsscmap  20631  rhmsscrnghm  20637  ringcsect  20642  funcringcsetc  20646  rngcrescrhm  20656  rhmsubclem1  20657  fldc  20756  fldhmsubc  20757  acsfn1p  20771  lspextmo  21046  2idlval  21244  pjfval  21681  pjpm  21683  aspsubrg  21850  psrbagsn  22039  ofco2  22434  basdif0  22936  tgval2  22939  eltg3  22945  tgcl  22952  tgdom  22961  tgidm  22963  ppttop  22990  epttop  22992  ntropn  23032  ntrin  23044  mretopd  23075  neiptoptop  23114  restfpw  23162  neitr  23163  restcls  23164  cncls  23257  cnpresti  23271  cnprest  23272  cmpsublem  23382  cmpsub  23383  fiuncmp  23387  indisconn  23401  connsub  23404  iunconnlem  23410  islly2  23467  cldllycmp  23478  kgentopon  23521  ptbasfi  23564  ptcnplem  23604  txcnmpt  23607  txcmplem2  23625  hausdiag  23628  txkgen  23635  xkococnlem  23642  qtoptop2  23682  basqtop  23694  fbssfi  23820  filin  23837  infil  23846  fbasrn  23867  fgtr  23873  ufprim  23892  flimrest  23966  txflf  23989  fclsrest  24007  alexsubALTlem4  24033  tsmsres  24127  tsmsxplem1  24136  ustund  24205  trust  24212  utoptop  24217  restutop  24220  cfiluweak  24277  xmetres  24347  metres  24348  blin2  24412  setsmstopn  24461  metrest  24507  ressxms  24508  tgioo  24779  xrsmopn  24796  reconnlem1  24810  xrge0tsms  24818  tcphcph  25222  cfilresi  25280  cfilres  25281  caussi  25282  causs  25283  relcmpcmet  25303  minveclem4a  25415  ismbl2  25512  cmmbl  25519  nulmbl2  25521  unmbl  25522  shftmbl  25523  volinun  25531  voliunlem1  25535  voliunlem2  25536  ioombl1lem4  25546  ioombl1  25547  uniioombllem2  25568  uniioombllem3  25570  uniioombllem4  25571  uniioombllem5  25572  uniioombl  25574  volivth  25592  vitalilem3  25595  vitalilem4  25596  vitalilem5  25597  vitali  25598  mbfadd  25646  mbfsub  25647  i1fadd  25680  itg1addlem2  25682  itg1addlem4  25684  itg1addlem5  25685  itg1climres  25699  mbfmul  25711  itg2splitlem  25733  itg2split  25734  limcresi  25870  limciun  25879  dvreslem  25894  dvres2lem  25895  dvres  25896  dvres3a  25899  dvaddbr  25923  dvmulbr  25924  dvfsumle  26006  dvfsumabs  26008  ig1peu  26158  pilem2  26435  pilem3  26436  rlimcnp2  26948  ppisval  27085  ppifi  27087  ppiprm  27132  chtprm  27134  chtdif  27139  efchtdvds  27140  ppidif  27144  ppiltx  27158  prmorcht  27159  ppiub  27185  chtlepsi  27187  pclogsum  27196  vmasum  27197  chpval2  27199  chpub  27201  2sqlem8  27407  chebbnd1lem1  27450  chtppilimlem1  27454  rpvmasum2  27493  dchrisum0re  27494  rplogsum  27508  dirith2  27509  nosupbnd1lem1  27690  nosupbnd2  27698  noinfbnd1lem1  27705  axtgcgrrflx  28548  axtgcgrid  28549  axtgsegcon  28550  axtg5seg  28551  axtgbtwnid  28552  axtgpasch  28553  axtgcont1  28554  phnv  30903  minvecolem2  30964  minvecolem3  30965  minvecolem5  30970  minvecolem6  30971  minvecolem7  30972  hlimcaui  31325  chdmm1i  31566  chabs1  31605  chabs2  31606  ledii  31625  lejdii  31627  pjoml4i  31676  cmbr3i  31689  cmbr4i  31690  cmm1i  31695  osumcor2i  31733  3oalem4  31754  pjssmii  31770  pjocini  31787  pjini  31788  mayete3i  31817  riesz4  32153  riesz1  32154  cnlnadjeui  32166  cnlnadjeu  32167  cnlnssadj  32169  nmopadjlei  32177  pjin1i  32281  pjclem1  32284  stji1i  32331  stm1i  32332  dmdbr2  32392  ssmd1  32400  mdslj2i  32409  mdsl2bi  32412  mdslmd1lem1  32414  mdslmd2i  32419  atomli  32471  atcvat4i  32486  sumdmdlem2  32508  dmdbr5ati  32511  dmdbr6ati  32512  dmdbr7ati  32513  indifbi  32608  disjxpin  32677  imadifxp  32690  nfpconfp  32724  off2  32733  ffsrn  32820  indsumin  32940  indf1ofs  32945  gsummptres  33133  xrge0tsmsd  33154  idlinsubrg  33514  ordtrestNEW  34105  qqhnm  34174  qqhcn  34175  rrhre  34205  esumval  34230  esumel  34231  gsumesum  34243  esumlub  34244  esumcst  34247  esumfsup  34254  esumpcvgval  34262  esumcvg  34270  sigainb  34320  ldgenpisyslem1  34347  measinb2  34407  sibfinima  34523  sibfof  34524  eulerpartlemelr  34541  eulerpartlem1  34551  eulerpartgbij  34556  eulerpartlemgu  34561  eulerpartlemgs2  34564  sseqf  34576  ballotlemfelz  34675  ballotlemfp1  34676  reprinrn  34802  reprinfz1  34806  hgt750lemd  34832  bnj1292  34997  connpconn  35463  iccllysconn  35478  cvmsss2  35502  cvmcov2  35503  cvmopnlem  35506  cvmliftmolem2  35510  cvmliftlem15  35526  cvmlift2lem12  35542  mvrsfpw  35734  msrf  35770  elmsta  35776  mthmpps  35810  nepss  35946  dfon2lem4  36012  txpss3v  36104  fixssdm  36132  fixssrn  36133  limitssson  36137  fneer  36581  neibastop1  36587  neibastop2lem  36588  filnetlem3  36608  ontopbas  36656  bj-disj2r  37381  bj-restpw  37450  bj-discrmoore  37469  bj-idres  37520  bj-fvsnun2  37616  bj-ablssgrp  37636  bj-fldssdrng  37648  taupilemrplb  37680  taupilem2  37682  taupi  37683  ptrest  37986  poimirlem29  38016  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  mbfposadd  38034  sstotbnd2  38141  ssbnd  38155  heibor1lem  38176  heiborlem1  38178  heiborlem3  38180  heiborlem5  38182  heiborlem6  38183  heiborlem10  38187  heibor  38188  opidonOLD  38219  exidcl  38243  flddivrng  38366  iss2  38711  xrnss3v  38748  refrelsredund2  39084  lshpinN  39481  lcvexchlem5  39530  pmodlem2  40339  pmod1i  40340  pmodN  40342  osumcllem7N  40454  pexmidlem4N  40465  pl42lem3N  40473  djaclN  41628  dihoml4c  41868  dochdmj1  41882  djhcl  41892  dochexmidlem4  41955  mapd1o  42140  mapdin  42154  unitscyglem5  42684  redvmptabs  42837  elrfi  43143  elrfirn  43144  elrfirn2  43145  ismrcd1  43147  istopclsd  43149  isnacs2  43155  mrefg3  43157  isnacs3  43159  diophrw  43208  diophin  43221  aomclem2  43500  islmodfg  43514  lsmfgcl  43519  lmhmfgima  43529  lmhmfgsplit  43531  lmhmlnmsplit  43532  pwfi2f1o  43541  hbt  43575  ofoafg  43799  harval3  43982  elinintrab  44021  trrelind  44109  clsk3nimkb  44484  isotone2  44493  ismnushort  44745  onfrALTlem2  44990  onfrALTlem2VD  45332  wfac8prim  45446  unirestss  45571  inmap  45654  fsumiunss  46020  islptre  46064  sumnnodd  46075  limclner  46094  liminfval4  46232  liminfval3  46233  cnrefiisplem  46272  cncfuni  46329  ismbl3  46429  ismbl4  46436  fouriersw  46674  qndenserrnbllem  46737  salincl  46767  salgencntex  46786  sge0less  46835  sge0resplit  46849  sge0split  46852  sge0iunmptlemre  46858  carageniuncllem1  46964  carageniuncllem2  46965  caragenel2d  46975  hspmbllem3  47071  hspmbl  47072  ovolval2lem  47086  sssmf  47181  smfaddlem1  47206  smflimlem2  47215  smflimlem3  47216  smflimlem4  47217  smfres  47233  smfmullem4  47237  smfsuplem1  47254  fcoreslem2  47527  indprmfz  48108  ppivalnn  48110  rngcrescrhmALTV  48771  rhmsubcALTVlem1  48772  funcringcsetcALTV2lem9  48789  fldcALTV  48823  fldhmsubcALTV  48824  iscnrm3llem2  49440  uptrlem1  49700  uptrlem2  49701  uptrlem3  49702  uptra  49705  uptrar  49706  uobeqw  49709  uptr2  49711  uptr2a  49712  fucoppcfunc  49902  setrec2fun  50182