Theorem inss1 4188

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

Syntax hints:   ∩ cin 3903   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-ss 3921

This theorem is referenced by:  inss2  4189  ssinss1  4197  ssinss1OLD  4198  unabs  4217  nssinpss  4219  dfin4  4230  inv1  4352  disjdif  4426  ifssun  4498  uniin  4889  uniintsn  4943  wefrc  5641  relin1  5785  resss  5987  resindm  6016  resmpt3  6027  rnin  6130  cnvcnvssOLD  6181  resdmss  6222  resssxp  6257  predss  6296  ordtri3or  6378  onfr  6385  ordelinel  6449  funin  6597  funimass2  6604  fnresin1  6646  fnres  6648  fresin  6733  fresaun  6735  nfvres  6905  ssimaex  6952  fneqeql2  7028  fnfvimad  7218  funiunfv  7232  isoini2  7323  ofrfvalg  7668  ofval  7671  ofrval  7672  off  7678  ofres  7679  ofco  7685  fparlem3  8093  fparlem4  8094  frrlem4  8270  frrlem13  8279  smores  8323  smores2  8325  tfrlem5  8350  pmresg  8852  sbthlem7  9065  sbthcl  9071  infi  9214  imafi  9259  ixpfi2  9293  unifpw  9298  elfiun  9376  dffi3  9377  marypha1lem  9379  ordtypelem6  9471  ordtypelem7  9472  ordtypelem8  9473  wdomima2g  9534  frmin  9707  frrlem15  9715  frrlem16  9716  tskwe  9908  ackbij1lem15  10189  ackbij1lem16  10190  fin23lem23  10283  fin23lem22  10284  fin23lem19  10293  brdom3  10485  brdom5  10486  brdom4  10487  imadomg  10491  fpwwe2lem11  10599  canthp1lem2  10611  wunin  10671  tskin  10717  gruima  10760  ingru  10773  gruina  10776  grur1a  10777  nqerf  10888  nqerrel  10890  hashun3  14397  hashin  14424  hashdif  14426  xptrrel  14993  rexanuz  15373  limsupgle  15504  rlimres  15585  lo1res  15586  lo1resb  15591  rlimresb  15592  o1resb  15593  lo1eq  15595  rlimeq  15596  o1of2  15640  o1rlimmul  15646  isercolllem2  15693  isercolllem3  15694  isercoll  15695  incexclem  15866  incexc  15867  bitsinvp1  16483  sadcaddlem  16491  sadadd2lem  16493  sadadd3  16495  sadaddlem  16500  sadasslem  16504  sadeq  16506  bitsres  16507  smuval2  16516  smupval  16522  smueqlem  16524  smumul  16527  ramub2  17050  ramub1lem2  17063  fvsetsid  17204  ressbasss2  17277  ressinbas  17281  ressress  17283  submre  17633  isacs1i  17689  mreacs  17690  acsfn  17691  invss  17794  sscres  17856  catcisolem  18143  catciso  18144  isacs5lem  18577  psss  18612  tsrss  18621  tsrdir  18636  sylow2a  19659  lsmmod  19715  gsumzres  19949  gsumzaddlem  19961  dprddisj2  20081  ablfac1eu  20115  isunit  20422  rngcbas  20671  rngchomfval  20672  rngccofval  20676  dfrngc2  20678  rnghmsscmap2  20679  rnghmsscmap  20680  rngcsect  20686  funcrngcsetc  20690  ringcbas  20700  ringchomfval  20701  ringccofval  20705  dfringc2  20707  rhmsscmap2  20708  rhmsscmap  20709  rhmsscrnghm  20715  ringcsect  20720  funcringcsetc  20724  rngcrescrhm  20734  rhmsubclem1  20735  fldc  20833  fldhmsubc  20834  acsfn1p  20848  lspextmo  21123  2idlval  21321  pjfval  21758  pjpm  21760  aspsubrg  21927  psrbagsn  22116  ofco2  22511  basdif0  23013  tgval2  23016  eltg3  23022  tgcl  23029  tgdom  23038  tgidm  23040  ppttop  23067  epttop  23069  ntropn  23109  ntrin  23121  mretopd  23152  neiptoptop  23191  restfpw  23239  neitr  23240  restcls  23241  cncls  23334  cnpresti  23348  cnprest  23349  cmpsublem  23459  cmpsub  23460  fiuncmp  23464  indisconn  23478  connsub  23481  iunconnlem  23487  islly2  23544  cldllycmp  23555  kgentopon  23598  ptbasfi  23641  ptcnplem  23681  txcnmpt  23684  txcmplem2  23702  hausdiag  23705  txkgen  23712  xkococnlem  23719  qtoptop2  23759  basqtop  23771  fbssfi  23897  filin  23914  infil  23923  fbasrn  23944  fgtr  23950  ufprim  23969  flimrest  24043  txflf  24066  fclsrest  24084  alexsubALTlem4  24110  tsmsres  24204  tsmsxplem1  24213  ustund  24282  trust  24289  utoptop  24294  restutop  24297  cfiluweak  24354  xmetres  24424  metres  24425  blin2  24489  setsmstopn  24538  metrest  24584  ressxms  24585  tgioo  24856  xrsmopn  24873  reconnlem1  24887  xrge0tsms  24895  tcphcph  25299  cfilresi  25357  cfilres  25358  caussi  25359  causs  25360  relcmpcmet  25380  minveclem4a  25492  ismbl2  25589  cmmbl  25596  nulmbl2  25598  unmbl  25599  shftmbl  25600  volinun  25608  voliunlem1  25612  voliunlem2  25613  ioombl1lem4  25623  ioombl1  25624  uniioombllem2  25645  uniioombllem3  25647  uniioombllem4  25648  uniioombllem5  25649  uniioombl  25651  volivth  25669  vitalilem3  25672  vitalilem4  25673  vitalilem5  25674  vitali  25675  mbfadd  25723  mbfsub  25724  i1fadd  25757  itg1addlem2  25759  itg1addlem4  25761  itg1addlem5  25762  itg1climres  25776  mbfmul  25788  itg2splitlem  25810  itg2split  25811  limcresi  25947  limciun  25956  dvreslem  25971  dvres2lem  25972  dvres  25973  dvres3a  25976  dvaddbr  26000  dvmulbr  26001  dvfsumle  26083  dvfsumabs  26085  ig1peu  26235  pilem2  26515  pilem3  26516  rlimcnp2  27031  ppisval  27168  ppifi  27170  ppiprm  27215  chtprm  27217  chtdif  27222  efchtdvds  27223  ppidif  27227  ppiltx  27241  prmorcht  27242  ppiub  27268  chtlepsi  27270  pclogsum  27279  vmasum  27280  chpval2  27282  chpub  27284  2sqlem8  27490  chebbnd1lem1  27533  chtppilimlem1  27537  rpvmasum2  27576  dchrisum0re  27577  rplogsum  27591  dirith2  27592  nosupbnd1lem1  27772  nosupbnd2  27780  noinfbnd1lem1  27787  axtgcgrrflx  28631  axtgcgrid  28632  axtgsegcon  28633  axtg5seg  28634  axtgbtwnid  28635  axtgpasch  28636  axtgcont1  28637  phnv  31017  minvecolem2  31078  minvecolem3  31079  minvecolem5  31084  minvecolem6  31085  minvecolem7  31086  hlimcaui  31439  chdmm1i  31680  chabs1  31719  chabs2  31720  ledii  31739  lejdii  31741  pjoml4i  31790  cmbr3i  31803  cmbr4i  31804  cmm1i  31809  osumcor2i  31847  3oalem4  31868  pjssmii  31884  pjocini  31901  pjini  31902  mayete3i  31931  riesz4  32267  riesz1  32268  cnlnadjeui  32280  cnlnadjeu  32281  cnlnssadj  32283  nmopadjlei  32291  pjin1i  32395  pjclem1  32398  stji1i  32445  stm1i  32446  dmdbr2  32506  ssmd1  32514  mdslj2i  32523  mdsl2bi  32526  mdslmd1lem1  32528  mdslmd2i  32533  atomli  32585  atcvat4i  32600  sumdmdlem2  32622  dmdbr5ati  32625  dmdbr6ati  32626  dmdbr7ati  32627  indifbi  32719  disjxpin  32788  imadifxp  32801  nfpconfp  32834  off2  32843  ffsrn  32930  indsumin  33039  indf1ofs  33044  gsummptres  33232  xrge0tsmsd  33253  idlinsubrg  33617  ordtrestNEW  34218  qqhnm  34287  qqhcn  34288  rrhre  34318  esumval  34343  esumel  34344  gsumesum  34356  esumlub  34357  esumcst  34360  esumfsup  34367  esumpcvgval  34375  esumcvg  34383  sigainb  34433  ldgenpisyslem1  34460  measinb2  34520  sibfinima  34636  sibfof  34637  eulerpartlemelr  34654  eulerpartlem1  34664  eulerpartgbij  34669  eulerpartlemgu  34674  eulerpartlemgs2  34677  sseqf  34689  ballotlemfelz  34788  ballotlemfp1  34789  reprinrn  34912  reprinfz1  34916  hgt750lemd  34942  bnj1292  35110  connpconn  35585  iccllysconn  35600  cvmsss2  35624  cvmcov2  35625  cvmopnlem  35628  cvmliftmolem2  35632  cvmliftlem15  35648  cvmlift2lem12  35664  mvrsfpw  35856  msrf  35892  elmsta  35898  mthmpps  35932  nepss  36068  dfon2lem4  36134  txpss3v  36226  fixssdm  36254  fixssrn  36255  limitssson  36259  fneer  36713  neibastop1  36719  neibastop2lem  36720  filnetlem3  36740  ontopbas  36788  bj-disj2r  37513  bj-restpw  37582  bj-discrmoore  37601  bj-idres  37652  bj-fvsnun2  37748  bj-ablssgrp  37768  bj-fldssdrng  37780  taupilemrplb  37812  taupilem2  37814  taupi  37815  ptrest  38118  poimirlem29  38148  mblfinlem3  38158  mblfinlem4  38159  ismblfin  38160  mbfposadd  38166  sstotbnd2  38273  ssbnd  38287  heibor1lem  38308  heiborlem1  38310  heiborlem3  38312  heiborlem5  38314  heiborlem6  38315  heiborlem10  38319  heibor  38320  opidonOLD  38351  exidcl  38375  flddivrng  38498  iss2  38843  xrnss3v  38880  refrelsredund2  39216  lshpinN  39613  lcvexchlem5  39662  pmodlem2  40471  pmod1i  40472  pmodN  40474  osumcllem7N  40586  pexmidlem4N  40597  pl42lem3N  40605  djaclN  41760  dihoml4c  42000  dochdmj1  42014  djhcl  42024  dochexmidlem4  42087  mapd1o  42272  mapdin  42286  unitscyglem5  42816  redvmptabs  42969  elrfi  43275  elrfirn  43276  elrfirn2  43277  ismrcd1  43279  istopclsd  43281  isnacs2  43287  mrefg3  43289  isnacs3  43291  diophrw  43340  diophin  43353  aomclem2  43632  islmodfg  43646  lsmfgcl  43651  lmhmfgima  43661  lmhmfgsplit  43663  lmhmlnmsplit  43664  pwfi2f1o  43673  hbt  43707  ofoafg  43931  harval3  44114  elinintrab  44153  trrelind  44241  clsk3nimkb  44616  isotone2  44625  ismnushort  44877  onfrALTlem2  45122  onfrALTlem2VD  45464  wfac8prim  45578  unirestss  45702  inmap  45785  fsumiunss  46151  islptre  46195  sumnnodd  46206  limclner  46225  liminfval4  46363  liminfval3  46364  cnrefiisplem  46403  cncfuni  46460  ismbl3  46560  ismbl4  46567  fouriersw  46805  qndenserrnbllem  46868  salincl  46898  salgencntex  46917  sge0less  46966  sge0resplit  46980  sge0split  46983  sge0iunmptlemre  46989  carageniuncllem1  47095  carageniuncllem2  47096  caragenel2d  47106  hspmbllem3  47202  hspmbl  47203  ovolval2lem  47217  sssmf  47312  smfaddlem1  47337  smflimlem2  47346  smflimlem3  47347  smflimlem4  47348  smfres  47364  smfmullem4  47368  smfsuplem1  47385  fcoreslem2  47658  indprmfz  48239  ppivalnn  48241  rngcrescrhmALTV  48902  rhmsubcALTVlem1  48903  funcringcsetcALTV2lem9  48920  fldcALTV  48954  fldhmsubcALTV  48955  iscnrm3llem2  49571  uptrlem1  49831  uptrlem2  49832  uptrlem3  49833  uptra  49836  uptrar  49837  uobeqw  49840  uptr2  49842  uptr2a  49843  fucoppcfunc  50033  setrec2fun  50313