Theorem inss1 4203

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

Syntax hints:   ∩ cin 3916   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  inss2  4204  ssinss1  4212  unabs  4231  nssinpss  4233  dfin4  4244  inv1  4364  disjdif  4438  ifssun  4509  uniintsn  4952  wefrc  5635  relin1  5778  resss  5975  resmpt3  6012  cnvcnvss  6170  resdmss  6211  resssxp  6246  predss  6285  ordtri3or  6367  onfr  6374  ordelinel  6438  funin  6595  funimass2  6602  fnresin1  6646  fnres  6648  fresin  6732  fresaun  6734  nfvres  6902  ssimaex  6949  fneqeql2  7022  fnfvimad  7211  funiunfv  7225  isoini2  7317  ofrfvalg  7664  ofval  7667  ofrval  7668  off  7674  ofres  7675  ofco  7681  fparlem3  8096  fparlem4  8097  frrlem4  8271  frrlem13  8280  smores  8324  smores2  8326  tfrlem5  8351  pmresg  8846  sbthlem7  9063  sbthcl  9069  infi  9220  imafi  9271  ixpfi2  9308  unifpw  9313  elfiun  9388  dffi3  9389  marypha1lem  9391  ordtypelem6  9483  ordtypelem7  9484  ordtypelem8  9485  wdomima2g  9546  frmin  9709  frrlem15  9717  frrlem16  9718  tskwe  9910  ackbij1lem15  10193  ackbij1lem16  10194  fin23lem23  10286  fin23lem22  10287  fin23lem19  10296  brdom3  10488  brdom5  10489  brdom4  10490  imadomg  10494  fpwwe2lem11  10601  canthp1lem2  10613  wunin  10673  tskin  10719  gruima  10762  ingru  10775  gruina  10778  grur1a  10779  nqerf  10890  nqerrel  10892  hashun3  14356  hashin  14383  hashdif  14385  xptrrel  14953  rexanuz  15319  limsupgle  15450  rlimres  15531  lo1res  15532  lo1resb  15537  rlimresb  15538  o1resb  15539  lo1eq  15541  rlimeq  15542  o1of2  15586  o1rlimmul  15592  isercolllem2  15639  isercolllem3  15640  isercoll  15641  incexclem  15809  incexc  15810  bitsinvp1  16426  sadcaddlem  16434  sadadd2lem  16436  sadadd3  16438  sadaddlem  16443  sadasslem  16447  sadeq  16449  bitsres  16450  smuval2  16459  smupval  16465  smueqlem  16467  smumul  16470  ramub2  16992  ramub1lem2  17005  fvsetsid  17145  ressbasss2  17218  ressinbas  17222  ressress  17224  submre  17573  isacs1i  17625  mreacs  17626  acsfn  17627  invss  17730  sscres  17792  catcisolem  18079  catciso  18080  isacs5lem  18511  psss  18546  tsrss  18555  tsrdir  18570  sylow2a  19556  lsmmod  19612  gsumzres  19846  gsumzaddlem  19858  dprddisj2  19978  ablfac1eu  20012  isunit  20289  rngcbas  20537  rngchomfval  20538  rngccofval  20542  dfrngc2  20544  rnghmsscmap2  20545  rnghmsscmap  20546  rngcsect  20552  funcrngcsetc  20556  ringcbas  20566  ringchomfval  20567  ringccofval  20571  dfringc2  20573  rhmsscmap2  20574  rhmsscmap  20575  rhmsscrnghm  20581  ringcsect  20586  funcringcsetc  20590  rngcrescrhm  20600  rhmsubclem1  20601  fldc  20700  fldhmsubc  20701  acsfn1p  20715  lspextmo  20970  2idlval  21168  pjfval  21622  pjpm  21624  aspsubrg  21792  psrbagsn  21977  ofco2  22345  basdif0  22847  tgval2  22850  eltg3  22856  tgcl  22863  tgdom  22872  tgidm  22874  ppttop  22901  epttop  22903  ntropn  22943  ntrin  22955  mretopd  22986  neiptoptop  23025  restfpw  23073  neitr  23074  restcls  23075  cncls  23168  cnpresti  23182  cnprest  23183  cmpsublem  23293  cmpsub  23294  fiuncmp  23298  indisconn  23312  connsub  23315  iunconnlem  23321  islly2  23378  cldllycmp  23389  kgentopon  23432  ptbasfi  23475  ptcnplem  23515  txcnmpt  23518  txcmplem2  23536  hausdiag  23539  txkgen  23546  xkococnlem  23553  qtoptop2  23593  basqtop  23605  fbssfi  23731  filin  23748  infil  23757  fbasrn  23778  fgtr  23784  ufprim  23803  flimrest  23877  txflf  23900  fclsrest  23918  alexsubALTlem4  23944  tsmsres  24038  tsmsxplem1  24047  ustund  24116  trust  24124  utoptop  24129  restutop  24132  cfiluweak  24189  xmetres  24259  metres  24260  blin2  24324  setsmstopn  24373  metrest  24419  ressxms  24420  tgioo  24691  xrsmopn  24708  reconnlem1  24722  xrge0tsms  24730  tcphcph  25144  cfilresi  25202  cfilres  25203  caussi  25204  causs  25205  relcmpcmet  25225  minveclem4a  25337  ismbl2  25435  cmmbl  25442  nulmbl2  25444  unmbl  25445  shftmbl  25446  volinun  25454  voliunlem1  25458  voliunlem2  25459  ioombl1lem4  25469  ioombl1  25470  uniioombllem2  25491  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombl  25497  volivth  25515  vitalilem3  25518  vitalilem4  25519  vitalilem5  25520  vitali  25521  mbfadd  25569  mbfsub  25570  i1fadd  25603  itg1addlem2  25605  itg1addlem4  25607  itg1addlem5  25608  itg1climres  25622  mbfmul  25634  itg2splitlem  25656  itg2split  25657  limcresi  25793  limciun  25802  dvreslem  25817  dvres2lem  25818  dvres  25819  dvres3a  25822  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  ig1peu  26087  pilem2  26369  pilem3  26370  rlimcnp2  26883  ppisval  27021  ppifi  27023  ppiprm  27068  chtprm  27070  chtdif  27075  efchtdvds  27076  ppidif  27080  ppiltx  27094  prmorcht  27095  ppiub  27122  chtlepsi  27124  pclogsum  27133  vmasum  27134  chpval2  27136  chpub  27138  2sqlem8  27344  chebbnd1lem1  27387  chtppilimlem1  27391  rpvmasum2  27430  dchrisum0re  27431  rplogsum  27445  dirith2  27446  nosupbnd1lem1  27627  nosupbnd2  27635  noinfbnd1lem1  27642  axtgcgrrflx  28396  axtgcgrid  28397  axtgsegcon  28398  axtg5seg  28399  axtgbtwnid  28400  axtgpasch  28401  axtgcont1  28402  phnv  30750  minvecolem2  30811  minvecolem3  30812  minvecolem5  30817  minvecolem6  30818  minvecolem7  30819  hlimcaui  31172  chdmm1i  31413  chabs1  31452  chabs2  31453  ledii  31472  lejdii  31474  pjoml4i  31523  cmbr3i  31536  cmbr4i  31537  cmm1i  31542  osumcor2i  31580  3oalem4  31601  pjssmii  31617  pjocini  31634  pjini  31635  mayete3i  31664  riesz4  32000  riesz1  32001  cnlnadjeui  32013  cnlnadjeu  32014  cnlnssadj  32016  nmopadjlei  32024  pjin1i  32128  pjclem1  32131  stji1i  32178  stm1i  32179  dmdbr2  32239  ssmd1  32247  mdslj2i  32256  mdsl2bi  32259  mdslmd1lem1  32261  mdslmd2i  32266  atomli  32318  atcvat4i  32333  sumdmdlem2  32355  dmdbr5ati  32358  dmdbr6ati  32359  dmdbr7ati  32360  indifbi  32456  disjxpin  32524  imadifxp  32537  nfpconfp  32563  off2  32572  ffsrn  32659  indsumin  32792  indf1ofs  32796  gsummptres  32999  xrge0tsmsd  33009  idlinsubrg  33409  ordtrestNEW  33918  qqhnm  33987  qqhcn  33988  rrhre  34018  esumval  34043  esumel  34044  gsumesum  34056  esumlub  34057  esumcst  34060  esumfsup  34067  esumpcvgval  34075  esumcvg  34083  sigainb  34133  ldgenpisyslem1  34160  measinb2  34220  sibfinima  34337  sibfof  34338  eulerpartlemelr  34355  eulerpartlem1  34365  eulerpartgbij  34370  eulerpartlemgu  34375  eulerpartlemgs2  34378  sseqf  34390  ballotlemfelz  34489  ballotlemfp1  34490  reprinrn  34616  reprinfz1  34620  hgt750lemd  34646  bnj1292  34812  connpconn  35229  iccllysconn  35244  cvmsss2  35268  cvmcov2  35269  cvmopnlem  35272  cvmliftmolem2  35276  cvmliftlem15  35292  cvmlift2lem12  35308  mvrsfpw  35500  msrf  35536  elmsta  35542  mthmpps  35576  nepss  35712  dfon2lem4  35781  txpss3v  35873  fixssdm  35901  fixssrn  35902  limitssson  35906  fneer  36348  neibastop1  36354  neibastop2lem  36355  filnetlem3  36375  ontopbas  36423  bj-disj2r  37023  bj-restpw  37087  bj-discrmoore  37106  bj-idres  37155  bj-fvsnun2  37251  bj-ablssgrp  37271  bj-fldssdrng  37283  taupilemrplb  37315  taupilem2  37317  taupi  37318  ptrest  37620  poimirlem29  37650  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  mbfposadd  37668  sstotbnd2  37775  ssbnd  37789  heibor1lem  37810  heiborlem1  37812  heiborlem3  37814  heiborlem5  37816  heiborlem6  37817  heiborlem10  37821  heibor  37822  opidonOLD  37853  exidcl  37877  flddivrng  38000  iss2  38333  xrnss3v  38361  refrelsredund2  38631  lshpinN  38989  lcvexchlem5  39038  pmodlem2  39848  pmod1i  39849  pmodN  39851  osumcllem7N  39963  pexmidlem4N  39974  pl42lem3N  39982  djaclN  41137  dihoml4c  41377  dochdmj1  41391  djhcl  41401  dochexmidlem4  41464  mapd1o  41649  mapdin  41663  unitscyglem5  42194  redvmptabs  42355  elrfi  42689  elrfirn  42690  elrfirn2  42691  ismrcd1  42693  istopclsd  42695  isnacs2  42701  mrefg3  42703  isnacs3  42705  diophrw  42754  diophin  42767  aomclem2  43051  islmodfg  43065  lsmfgcl  43070  lmhmfgima  43080  lmhmfgsplit  43082  lmhmlnmsplit  43083  pwfi2f1o  43092  hbt  43126  ofoafg  43350  harval3  43534  elinintrab  43573  trrelind  43661  clsk3nimkb  44036  isotone2  44045  ismnushort  44297  onfrALTlem2  44543  onfrALTlem2VD  44885  wfac8prim  44999  unirestss  45125  inmap  45210  fsumiunss  45580  islptre  45624  sumnnodd  45635  limclner  45656  liminfval4  45794  liminfval3  45795  cnrefiisplem  45834  cncfuni  45891  ismbl3  45991  ismbl4  45998  fouriersw  46236  qndenserrnbllem  46299  salincl  46329  salgencntex  46348  sge0less  46397  sge0resplit  46411  sge0split  46414  sge0iunmptlemre  46420  carageniuncllem1  46526  carageniuncllem2  46527  caragenel2d  46537  hspmbllem3  46633  hspmbl  46634  ovolval2lem  46648  sssmf  46743  smfaddlem1  46768  smflimlem2  46777  smflimlem3  46778  smflimlem4  46779  smfres  46795  smfmullem4  46799  smfsuplem1  46816  fcoreslem2  47069  rngcrescrhmALTV  48272  rhmsubcALTVlem1  48273  funcringcsetcALTV2lem9  48290  fldcALTV  48324  fldhmsubcALTV  48325  iscnrm3llem2  48942  uptrlem1  49203  uptrlem2  49204  uptrlem3  49205  uptra  49208  uptrar  49209  uobeqw  49212  uptr2  49214  uptr2a  49215  fucoppcfunc  49405  setrec2fun  49685