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 3941	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Syntax hints:   ∩ cin 3904   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ss 3922

This theorem is referenced by:  inss2  4190  ssinss1  4198  ssinss1OLD  4199  unabs  4218  nssinpss  4220  dfin4  4231  inv1  4355  vvin  4366  ifssun  4505  uniin  4896  uniintsn  4950  wefrc  5655  relin1  5799  resss  6000  resindm  6029  resmpt3  6040  rnin  6143  cnvcnvssOLD  6193  resdmss  6236  resssxp  6271  predss  6310  ordtri3or  6393  onfr  6400  ordelinel  6464  funin  6612  funimass2  6619  fnresin1  6660  fnres  6662  fresin  6747  fresaun  6749  nfvres  6919  ssimaex  6966  fneqeql2  7042  fnfvimad  7232  funiunfv  7246  isoini2  7337  ofrfvalg  7682  ofval  7685  ofrval  7686  off  7692  ofres  7693  ofco  7699  fparlem3  8105  fparlem4  8106  frrlem4  8282  frrlem13  8291  smores  8335  smores2  8337  tfrlem5  8362  pmresg  8864  sbthlem7  9077  sbthcl  9083  infi  9226  imafi  9271  ixpfi2  9303  unifpw  9308  elfiun  9386  dffi3  9387  marypha1lem  9389  ordtypelem6  9481  ordtypelem7  9482  ordtypelem8  9483  wdomima2g  9544  frmin  9717  frrlem15  9725  frrlem16  9726  tskwe  9932  ackbij1lem15  10212  ackbij1lem16  10213  fin23lem23  10305  fin23lem22  10306  fin23lem19  10315  brdom3  10507  brdom5  10508  brdom4  10509  imadomg  10513  fpwwe2lem11  10621  canthp1lem2  10633  wunin  10693  tskin  10739  gruima  10782  ingru  10795  gruina  10798  grur1a  10799  nqerf  10910  nqerrel  10912  hashun3  14416  hashin  14444  hashdif  14446  xptrrel  15013  rexanuz  15393  limsupgle  15524  rlimres  15605  lo1res  15606  lo1resb  15611  rlimresb  15612  o1resb  15613  lo1eq  15615  rlimeq  15616  o1of2  15660  o1rlimmul  15666  isercolllem2  15713  isercolllem3  15714  isercoll  15715  incexclem  15886  incexc  15887  bitsinvp1  16502  sadcaddlem  16510  sadadd2lem  16512  sadadd3  16514  sadaddlem  16519  sadasslem  16523  sadeq  16525  bitsres  16526  smuval2  16535  smupval  16541  smueqlem  16543  smumul  16546  ramub2  17069  ramub1lem2  17082  fvsetsid  17223  ressbasss2  17296  ressinbas  17300  ressress  17302  submre  17652  isacs1i  17708  mreacs  17709  acsfn  17710  invss  17813  sscres  17875  catcisolem  18162  catciso  18163  isacs5lem  18596  psss  18631  tsrss  18640  tsrdir  18655  sylow2a  19684  lsmmod  19740  gsumzres  19974  gsumzaddlem  19986  dprddisj2  20106  ablfac1eu  20140  isunit  20451  rngcbas  20720  rngchomfval  20721  rngccofval  20725  dfrngc2  20727  rnghmsscmap2  20728  rnghmsscmap  20729  rngcsect  20735  funcrngcsetc  20739  ringcbas  20749  ringchomfval  20750  ringccofval  20754  dfringc2  20756  rhmsscmap2  20757  rhmsscmap  20758  rhmsscrnghm  20764  ringcsect  20769  funcringcsetc  20773  rngcrescrhm  20783  rhmsubclem1  20784  fldc  20887  fldhmsubc  20888  acsfn1p  20902  lspextmo  21177  2idlval  21390  pjfval  21856  pjpm  21858  aspsubrg  22025  psrbagsn  22214  ofco2  22608  basdif0  23110  tgval2  23113  eltg3  23119  tgcl  23126  tgdom  23135  tgidm  23137  ppttop  23164  epttop  23166  ntropn  23206  ntrin  23218  mretopd  23249  neiptoptop  23288  restfpw  23336  neitr  23337  restcls  23338  cncls  23431  cnpresti  23445  cnprest  23446  cmpsublem  23556  cmpsub  23557  fiuncmp  23561  indisconn  23575  connsub  23578  iunconnlem  23584  islly2  23641  cldllycmp  23652  kgentopon  23695  ptbasfi  23738  ptcnplem  23778  txcnmpt  23781  txcmplem2  23799  hausdiag  23802  txkgen  23809  xkococnlem  23816  qtoptop2  23856  basqtop  23868  fbssfi  23994  filin  24011  infil  24020  fbasrn  24041  fgtr  24047  ufprim  24066  flimrest  24140  txflf  24163  fclsrest  24181  alexsubALTlem4  24207  tsmsres  24301  tsmsxplem1  24310  ustund  24379  trust  24386  utoptop  24391  restutop  24394  cfiluweak  24451  xmetres  24521  metres  24522  blin2  24586  setsmstopn  24635  metrest  24681  ressxms  24682  tgioo  24953  xrsmopn  24970  reconnlem1  24984  xrge0tsms  24992  tcphcph  25396  cfilresi  25454  cfilres  25455  caussi  25456  causs  25457  relcmpcmet  25477  minveclem4a  25589  ismbl2  25686  cmmbl  25693  nulmbl2  25695  unmbl  25696  shftmbl  25697  volinun  25705  voliunlem1  25709  voliunlem2  25710  ioombl1lem4  25720  ioombl1  25721  uniioombllem2  25742  uniioombllem3  25744  uniioombllem4  25745  uniioombllem5  25746  uniioombl  25748  volivth  25766  vitalilem3  25769  vitalilem4  25770  vitalilem5  25771  vitali  25772  mbfadd  25820  mbfsub  25821  i1fadd  25854  itg1addlem2  25856  itg1addlem4  25858  itg1addlem5  25859  itg1climres  25873  mbfmul  25885  itg2splitlem  25907  itg2split  25908  limcresi  26044  limciun  26053  dvreslem  26068  dvres2lem  26069  dvres  26070  dvres3a  26073  dvaddbr  26097  dvmulbr  26098  dvfsumle  26180  dvfsumabs  26182  ig1peu  26332  pilem2  26615  pilem3  26616  rlimcnp2  27131  ppisval  27268  ppifi  27270  ppiprm  27315  chtprm  27317  chtdif  27322  efchtdvds  27323  ppidif  27327  ppiltx  27341  prmorcht  27342  ppiub  27368  chtlepsi  27370  pclogsum  27379  vmasum  27380  chpval2  27382  chpub  27384  2sqlem8  27590  chebbnd1lem1  27633  chtppilimlem1  27637  rpvmasum2  27676  dchrisum0re  27677  rplogsum  27691  dirith2  27692  nosupbnd1lem1  27872  nosupbnd2  27880  noinfbnd1lem1  27887  axtgcgrrflx  28731  axtgcgrid  28732  axtgsegcon  28733  axtg5seg  28734  axtgbtwnid  28735  axtgpasch  28736  axtgcont1  28737  phnv  31166  minvecolem2  31227  minvecolem3  31228  minvecolem5  31233  minvecolem6  31234  minvecolem7  31235  hlimcaui  31588  chdmm1i  31829  chabs1  31868  chabs2  31869  ledii  31888  lejdii  31890  pjoml4i  31939  cmbr3i  31952  cmbr4i  31953  cmm1i  31958  osumcor2i  31996  3oalem4  32017  pjssmii  32033  pjocini  32050  pjini  32051  mayete3i  32080  riesz4  32416  riesz1  32417  cnlnadjeui  32429  cnlnadjeu  32430  cnlnssadj  32432  nmopadjlei  32440  pjin1i  32544  pjclem1  32547  stji1i  32594  stm1i  32595  dmdbr2  32655  ssmd1  32663  mdslj2i  32672  mdsl2bi  32675  mdslmd1lem1  32677  mdslmd2i  32682  atomli  32734  atcvat4i  32749  sumdmdlem2  32771  dmdbr5ati  32774  dmdbr6ati  32775  dmdbr7ati  32776  indifbi  32866  disjxpin  32933  imadifxp  32946  nfpconfp  32977  off2  32986  ffsrn  33073  indsumin  33181  indf1ofs  33186  gsummptres  33372  xrge0tsmsd  33393  idlinsubrg  33739  ordtrestNEW  34311  qqhnm  34380  qqhcn  34381  rrhre  34411  esumval  34436  esumel  34437  gsumesum  34449  esumlub  34450  esumcst  34453  esumfsup  34460  esumpcvgval  34468  esumcvg  34476  sigainb  34526  ldgenpisyslem1  34553  measinb2  34613  sibfinima  34729  sibfof  34730  eulerpartlemelr  34747  eulerpartlem1  34757  eulerpartgbij  34762  eulerpartlemgu  34767  eulerpartlemgs2  34770  sseqf  34782  ballotlemfelz  34881  ballotlemfp1  34882  reprinrn  35005  reprinfz1  35009  hgt750lemd  35035  bnj1292  35203  connpconn  35727  iccllysconn  35742  cvmsss2  35766  cvmcov2  35767  cvmopnlem  35770  cvmliftmolem2  35774  cvmliftlem15  35790  cvmlift2lem12  35806  mvrsfpw  35998  msrf  36034  elmsta  36040  mthmpps  36074  nepss  36210  dfon2lem4  36276  txpss3v  36368  fixssdm  36396  fixssrn  36397  limitssson  36401  fneer  36864  neibastop1  36870  neibastop2lem  36871  filnetlem3  36891  ontopbas  36939  bj-disj2r  37664  bj-restpw  37734  bj-discrmoore  37753  bj-idres  37804  bj-fvsnun2  37900  bj-ablssgrp  37920  bj-fldssdrng  37932  taupilemrplb  37964  taupilem2  37966  taupi  37967  ptrest  38270  poimirlem29  38300  mblfinlem3  38310  mblfinlem4  38311  ismblfin  38312  mbfposadd  38318  sstotbnd2  38425  ssbnd  38439  heibor1lem  38460  heiborlem1  38462  heiborlem3  38464  heiborlem5  38466  heiborlem6  38467  heiborlem10  38471  heibor  38472  opidonOLD  38503  exidcl  38527  flddivrng  38650  iss2  38993  xrnss3v  39030  refrelsredund2  39366  lshpinN  39763  lcvexchlem5  39812  pmodlem2  40621  pmod1i  40622  pmodN  40624  osumcllem7N  40736  pexmidlem4N  40747  pl42lem3N  40755  djaclN  41910  dihoml4c  42150  dochdmj1  42164  djhcl  42174  dochexmidlem4  42237  mapd1o  42422  mapdin  42436  unitscyglem5  42966  redvmptabs  43121  elrfi  43425  elrfirn  43426  elrfirn2  43427  ismrcd1  43429  istopclsd  43431  isnacs2  43437  mrefg3  43439  isnacs3  43441  diophrw  43490  diophin  43503  aomclem2  43782  islmodfg  43796  lsmfgcl  43801  lmhmfgima  43811  lmhmfgsplit  43813  lmhmlnmsplit  43814  pwfi2f1o  43823  hbt  43857  ofoafg  44081  harval3  44264  elinintrab  44303  trrelind  44391  clsk3nimkb  44766  isotone2  44775  ismnushort  45011  onfrALTlem2  45255  onfrALTlem2VD  45597  wfac8prim  45711  unirestss  45842  inmap  45925  fsumiunss  46291  islptre  46335  sumnnodd  46346  limclner  46365  liminfval4  46503  liminfval3  46504  cnrefiisplem  46543  cncfuni  46600  ismbl3  46700  ismbl4  46707  fouriersw  46945  qndenserrnbllem  47008  salincl  47038  salgencntex  47057  sge0less  47106  sge0resplit  47120  sge0split  47123  sge0iunmptlemre  47129  carageniuncllem1  47235  carageniuncllem2  47236  caragenel2d  47246  hspmbllem3  47342  hspmbl  47343  ovolval2lem  47357  sssmf  47452  smfaddlem1  47477  smflimlem2  47486  smflimlem3  47487  smflimlem4  47488  smfres  47504  smfmullem4  47508  smfsuplem1  47525  fcoreslem2  47801  indprmfz  48382  ppivalnn  48384  rngcrescrhmALTV  49045  rhmsubcALTVlem1  49046  funcringcsetcALTV2lem9  49063  fldcALTV  49097  fldhmsubcALTV  49098  iscnrm3llem2  49728  uptrlem1  49988  uptrlem2  49989  uptrlem3  49990  uptra  49993  uptrar  49994  uobeqw  49997  uptr2  49999  uptr2a  50000  fucoppcfunc  50190  setrec2fun  50470