Theorem inss1 4244

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

Syntax hints:   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  inss2  4245  ssinss1  4253  unabs  4270  nssinpss  4272  dfin4  4283  inv1  4403  disjdif  4477  ifssun  4547  uniintsn  4989  wefrc  5682  relin1  5824  resss  6021  resmpt3  6057  cnvcnvss  6215  resdmss  6256  resssxp  6291  predss  6330  ordtri3or  6417  onfr  6424  ordelinel  6486  funin  6643  funimass2  6650  fnresin1  6693  fnres  6695  fresin  6777  fresaun  6779  nfvres  6947  ssimaex  6993  fneqeql2  7066  fnfvimad  7253  funiunfv  7267  isoini2  7358  ofrfvalg  7704  ofval  7707  ofrval  7708  off  7714  ofres  7715  ofco  7721  fparlem3  8137  fparlem4  8138  frrlem4  8312  frrlem13  8321  smores  8390  smores2  8392  tfrlem5  8418  pmresg  8908  sbthlem7  9127  sbthcl  9133  infi  9299  imafi  9350  ixpfi2  9387  unifpw  9392  elfiun  9467  dffi3  9468  marypha1lem  9470  ordtypelem6  9560  ordtypelem7  9561  ordtypelem8  9562  wdomima2g  9623  frmin  9786  frrlem15  9794  frrlem16  9795  tskwe  9987  ackbij1lem15  10270  ackbij1lem16  10271  fin23lem23  10363  fin23lem22  10364  fin23lem19  10373  brdom3  10565  brdom5  10566  brdom4  10567  imadomg  10571  fpwwe2lem11  10678  canthp1lem2  10690  wunin  10750  tskin  10796  gruima  10839  ingru  10852  gruina  10855  grur1a  10856  nqerf  10967  nqerrel  10969  hashun3  14419  hashin  14446  hashdif  14448  xptrrel  15015  rexanuz  15380  limsupgle  15509  rlimres  15590  lo1res  15591  lo1resb  15596  rlimresb  15597  o1resb  15598  lo1eq  15600  rlimeq  15601  o1of2  15645  o1rlimmul  15651  isercolllem2  15698  isercolllem3  15699  isercoll  15700  incexclem  15868  incexc  15869  bitsinvp1  16482  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  sadeq  16505  bitsres  16506  smuval2  16515  smupval  16521  smueqlem  16523  smumul  16526  ramub2  17047  ramub1lem2  17060  fvsetsid  17201  ressbasss2  17285  ressinbas  17290  ressress  17293  submre  17649  isacs1i  17701  mreacs  17702  acsfn  17703  invss  17808  sscres  17870  catcisolem  18163  catciso  18164  isacs5lem  18602  psss  18637  tsrss  18646  tsrdir  18661  sylow2a  19651  lsmmod  19707  gsumzres  19941  gsumzaddlem  19953  dprddisj2  20073  ablfac1eu  20107  isunit  20389  rngcbas  20637  rngchomfval  20638  rngccofval  20642  dfrngc2  20644  rnghmsscmap2  20645  rnghmsscmap  20646  rngcsect  20652  funcrngcsetc  20656  ringcbas  20666  ringchomfval  20667  ringccofval  20671  dfringc2  20673  rhmsscmap2  20674  rhmsscmap  20675  rhmsscrnghm  20681  ringcsect  20686  funcringcsetc  20690  rngcrescrhm  20700  rhmsubclem1  20701  fldc  20801  fldhmsubc  20802  acsfn1p  20816  lspextmo  21072  2idlval  21278  pjfval  21743  pjpm  21745  aspsubrg  21913  psrbagsn  22104  ofco2  22472  basdif0  22975  tgval2  22978  eltg3  22984  tgcl  22991  tgdom  23000  tgidm  23002  ppttop  23029  epttop  23031  ntropn  23072  ntrin  23084  mretopd  23115  neiptoptop  23154  restfpw  23202  neitr  23203  restcls  23204  cncls  23297  cnpresti  23311  cnprest  23312  cmpsublem  23422  cmpsub  23423  fiuncmp  23427  indisconn  23441  connsub  23444  iunconnlem  23450  islly2  23507  cldllycmp  23518  kgentopon  23561  ptbasfi  23604  ptcnplem  23644  txcnmpt  23647  txcmplem2  23665  hausdiag  23668  txkgen  23675  xkococnlem  23682  qtoptop2  23722  basqtop  23734  fbssfi  23860  filin  23877  infil  23886  fbasrn  23907  fgtr  23913  ufprim  23932  flimrest  24006  txflf  24029  fclsrest  24047  alexsubALTlem4  24073  tsmsres  24167  tsmsxplem1  24176  ustund  24245  trust  24253  utoptop  24258  restutop  24261  cfiluweak  24319  xmetres  24389  metres  24390  blin2  24454  setsmstopn  24505  metrest  24552  ressxms  24553  tgioo  24831  xrsmopn  24847  reconnlem1  24861  xrge0tsms  24869  tcphcph  25284  cfilresi  25342  cfilres  25343  caussi  25344  causs  25345  relcmpcmet  25365  minveclem4a  25477  ismbl2  25575  cmmbl  25582  nulmbl2  25584  unmbl  25585  shftmbl  25586  volinun  25594  voliunlem1  25598  voliunlem2  25599  ioombl1lem4  25609  ioombl1  25610  uniioombllem2  25631  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombl  25637  volivth  25655  vitalilem3  25658  vitalilem4  25659  vitalilem5  25660  vitali  25661  mbfadd  25709  mbfsub  25710  i1fadd  25743  itg1addlem2  25745  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  itg1climres  25763  mbfmul  25775  itg2splitlem  25797  itg2split  25798  limcresi  25934  limciun  25943  dvreslem  25958  dvres2lem  25959  dvres  25960  dvres3a  25963  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  ig1peu  26228  pilem2  26510  pilem3  26511  rlimcnp2  27023  ppisval  27161  ppifi  27163  ppiprm  27208  chtprm  27210  chtdif  27215  efchtdvds  27216  ppidif  27220  ppiltx  27234  prmorcht  27235  ppiub  27262  chtlepsi  27264  pclogsum  27273  vmasum  27274  chpval2  27276  chpub  27278  2sqlem8  27484  chebbnd1lem1  27527  chtppilimlem1  27531  rpvmasum2  27570  dchrisum0re  27571  rplogsum  27585  dirith2  27586  nosupbnd1lem1  27767  nosupbnd2  27775  noinfbnd1lem1  27782  axtgcgrrflx  28484  axtgcgrid  28485  axtgsegcon  28486  axtg5seg  28487  axtgbtwnid  28488  axtgpasch  28489  axtgcont1  28490  phnv  30842  minvecolem2  30903  minvecolem3  30904  minvecolem5  30909  minvecolem6  30910  minvecolem7  30911  hlimcaui  31264  chdmm1i  31505  chabs1  31544  chabs2  31545  ledii  31564  lejdii  31566  pjoml4i  31615  cmbr3i  31628  cmbr4i  31629  cmm1i  31634  osumcor2i  31672  3oalem4  31693  pjssmii  31709  pjocini  31726  pjini  31727  mayete3i  31756  riesz4  32092  riesz1  32093  cnlnadjeui  32105  cnlnadjeu  32106  cnlnssadj  32108  nmopadjlei  32116  pjin1i  32220  pjclem1  32223  stji1i  32270  stm1i  32271  dmdbr2  32331  ssmd1  32339  mdslj2i  32348  mdsl2bi  32351  mdslmd1lem1  32353  mdslmd2i  32358  atomli  32410  atcvat4i  32425  sumdmdlem2  32447  dmdbr5ati  32450  dmdbr6ati  32451  dmdbr7ati  32452  indifbi  32547  disjxpin  32607  imadifxp  32620  nfpconfp  32648  off2  32657  ffsrn  32746  gsummptres  33037  xrge0tsmsd  33047  idlinsubrg  33438  ordtrestNEW  33881  qqhnm  33952  qqhcn  33953  rrhre  33983  indsumin  34002  indf1ofs  34006  esumval  34026  esumel  34027  gsumesum  34039  esumlub  34040  esumcst  34043  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  sigainb  34116  ldgenpisyslem1  34143  measinb2  34203  sibfinima  34320  sibfof  34321  eulerpartlemelr  34338  eulerpartlem1  34348  eulerpartgbij  34353  eulerpartlemgu  34358  eulerpartlemgs2  34361  sseqf  34373  ballotlemfelz  34471  ballotlemfp1  34472  reprinrn  34611  reprinfz1  34615  hgt750lemd  34641  bnj1292  34807  connpconn  35219  iccllysconn  35234  cvmsss2  35258  cvmcov2  35259  cvmopnlem  35262  cvmliftmolem2  35266  cvmliftlem15  35282  cvmlift2lem12  35298  mvrsfpw  35490  msrf  35526  elmsta  35532  mthmpps  35566  nepss  35697  dfon2lem4  35767  txpss3v  35859  fixssdm  35887  fixssrn  35888  limitssson  35892  fneer  36335  neibastop1  36341  neibastop2lem  36342  filnetlem3  36362  ontopbas  36410  bj-disj2r  37010  bj-restpw  37074  bj-discrmoore  37093  bj-idres  37142  bj-fvsnun2  37238  bj-ablssgrp  37258  bj-fldssdrng  37270  taupilemrplb  37302  taupilem2  37304  taupi  37305  ptrest  37605  poimirlem29  37635  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  mbfposadd  37653  sstotbnd2  37760  ssbnd  37774  heibor1lem  37795  heiborlem1  37797  heiborlem3  37799  heiborlem5  37801  heiborlem6  37802  heiborlem10  37806  heibor  37807  opidonOLD  37838  exidcl  37862  flddivrng  37985  iss2  38325  xrnss3v  38353  refrelsredund2  38614  lshpinN  38970  lcvexchlem5  39019  pmodlem2  39829  pmod1i  39830  pmodN  39832  osumcllem7N  39944  pexmidlem4N  39955  pl42lem3N  39963  djaclN  41118  dihoml4c  41358  dochdmj1  41372  djhcl  41382  dochexmidlem4  41445  mapd1o  41630  mapdin  41644  unitscyglem5  42180  redvmptabs  42368  elrfi  42681  elrfirn  42682  elrfirn2  42683  ismrcd1  42685  istopclsd  42687  isnacs2  42693  mrefg3  42695  isnacs3  42697  diophrw  42746  diophin  42759  aomclem2  43043  islmodfg  43057  lsmfgcl  43062  lmhmfgima  43072  lmhmfgsplit  43074  lmhmlnmsplit  43075  pwfi2f1o  43084  hbt  43118  ofoafg  43343  harval3  43527  elinintrab  43566  trrelind  43654  clsk3nimkb  44029  isotone2  44038  ismnushort  44296  onfrALTlem2  44543  onfrALTlem2VD  44886  unirestss  45063  inmap  45151  fsumiunss  45530  islptre  45574  sumnnodd  45585  limclner  45606  liminfval4  45744  liminfval3  45745  cnrefiisplem  45784  cncfuni  45841  ismbl3  45941  ismbl4  45948  fouriersw  46186  qndenserrnbllem  46249  salincl  46279  salgencntex  46298  sge0less  46347  sge0resplit  46361  sge0split  46364  sge0iunmptlemre  46370  carageniuncllem1  46476  carageniuncllem2  46477  caragenel2d  46487  hspmbllem3  46583  hspmbl  46584  ovolval2lem  46598  sssmf  46693  smfaddlem1  46718  smflimlem2  46727  smflimlem3  46728  smflimlem4  46729  smfres  46745  smfmullem4  46749  smfsuplem1  46766  fcoreslem2  47013  rngcrescrhmALTV  48123  rhmsubcALTVlem1  48124  funcringcsetcALTV2lem9  48141  fldcALTV  48175  fldhmsubcALTV  48176  iscnrm3llem2  48746  setrec2fun  48922