Theorem inss1 4258

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

Syntax hints:   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  inss2  4259  ssinss1  4267  unabs  4284  nssinpss  4286  dfin4  4297  inv1  4421  disjdif  4495  ifssun  4565  uniintsn  5009  wefrc  5694  relin1  5836  resss  6031  resmpt3  6067  cnvcnvss  6225  resdmss  6266  resssxp  6301  predss  6340  ordtri3or  6427  onfr  6434  ordelinel  6496  funin  6654  funimass2  6661  fnresin1  6705  fnres  6707  fresin  6790  fresaun  6792  nfvres  6961  ssimaex  7007  fneqeql2  7080  fnfvimad  7271  funiunfv  7285  isoini2  7375  ofrfvalg  7722  ofval  7725  ofrval  7726  off  7732  ofres  7733  ofco  7738  fparlem3  8155  fparlem4  8156  frrlem4  8330  frrlem13  8339  smores  8408  smores2  8410  tfrlem5  8436  pmresg  8928  sbthlem7  9155  sbthcl  9161  infi  9330  imafi  9381  ixpfi2  9420  unifpw  9425  elfiun  9499  dffi3  9500  marypha1lem  9502  ordtypelem6  9592  ordtypelem7  9593  ordtypelem8  9594  wdomima2g  9655  frmin  9818  frrlem15  9826  frrlem16  9827  tskwe  10019  ackbij1lem15  10302  ackbij1lem16  10303  fin23lem23  10395  fin23lem22  10396  fin23lem19  10405  brdom3  10597  brdom5  10598  brdom4  10599  imadomg  10603  fpwwe2lem11  10710  canthp1lem2  10722  wunin  10782  tskin  10828  gruima  10871  ingru  10884  gruina  10887  grur1a  10888  nqerf  10999  nqerrel  11001  hashun3  14433  hashin  14460  hashdif  14462  xptrrel  15029  rexanuz  15394  limsupgle  15523  rlimres  15604  lo1res  15605  lo1resb  15610  rlimresb  15611  o1resb  15612  lo1eq  15614  rlimeq  15615  o1of2  15659  o1rlimmul  15665  isercolllem2  15714  isercolllem3  15715  isercoll  15716  incexclem  15884  incexc  15885  bitsinvp1  16495  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  bitsres  16519  smuval2  16528  smupval  16534  smueqlem  16536  smumul  16539  ramub2  17061  ramub1lem2  17074  fvsetsid  17215  ressbasss2  17299  ressinbas  17304  ressress  17307  submre  17663  isacs1i  17715  mreacs  17716  acsfn  17717  invss  17822  sscres  17884  catcisolem  18177  catciso  18178  isacs5lem  18615  psss  18650  tsrss  18659  tsrdir  18674  sylow2a  19661  lsmmod  19717  gsumzres  19951  gsumzaddlem  19963  dprddisj2  20083  ablfac1eu  20117  isunit  20399  rngcbas  20643  rngchomfval  20644  rngccofval  20648  dfrngc2  20650  rnghmsscmap2  20651  rnghmsscmap  20652  rngcsect  20658  funcrngcsetc  20662  ringcbas  20672  ringchomfval  20673  ringccofval  20677  dfringc2  20679  rhmsscmap2  20680  rhmsscmap  20681  rhmsscrnghm  20687  ringcsect  20692  funcringcsetc  20696  rngcrescrhm  20706  rhmsubclem1  20707  fldc  20807  fldhmsubc  20808  acsfn1p  20822  lspextmo  21078  2idlval  21284  pjfval  21749  pjpm  21751  aspsubrg  21919  psrbagsn  22110  ofco2  22478  basdif0  22981  tgval2  22984  eltg3  22990  tgcl  22997  tgdom  23006  tgidm  23008  ppttop  23035  epttop  23037  ntropn  23078  ntrin  23090  mretopd  23121  neiptoptop  23160  restfpw  23208  neitr  23209  restcls  23210  cncls  23303  cnpresti  23317  cnprest  23318  cmpsublem  23428  cmpsub  23429  fiuncmp  23433  indisconn  23447  connsub  23450  iunconnlem  23456  islly2  23513  cldllycmp  23524  kgentopon  23567  ptbasfi  23610  ptcnplem  23650  txcnmpt  23653  txcmplem2  23671  hausdiag  23674  txkgen  23681  xkococnlem  23688  qtoptop2  23728  basqtop  23740  fbssfi  23866  filin  23883  infil  23892  fbasrn  23913  fgtr  23919  ufprim  23938  flimrest  24012  txflf  24035  fclsrest  24053  alexsubALTlem4  24079  tsmsres  24173  tsmsxplem1  24182  ustund  24251  trust  24259  utoptop  24264  restutop  24267  cfiluweak  24325  xmetres  24395  metres  24396  blin2  24460  setsmstopn  24511  metrest  24558  ressxms  24559  tgioo  24837  xrsmopn  24853  reconnlem1  24867  xrge0tsms  24875  tcphcph  25290  cfilresi  25348  cfilres  25349  caussi  25350  causs  25351  relcmpcmet  25371  minveclem4a  25483  ismbl2  25581  cmmbl  25588  nulmbl2  25590  unmbl  25591  shftmbl  25592  volinun  25600  voliunlem1  25604  voliunlem2  25605  ioombl1lem4  25615  ioombl1  25616  uniioombllem2  25637  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  uniioombl  25643  volivth  25661  vitalilem3  25664  vitalilem4  25665  vitalilem5  25666  vitali  25667  mbfadd  25715  mbfsub  25716  i1fadd  25749  itg1addlem2  25751  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  itg1climres  25769  mbfmul  25781  itg2splitlem  25803  itg2split  25804  limcresi  25940  limciun  25949  dvreslem  25964  dvres2lem  25965  dvres  25966  dvres3a  25969  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  ig1peu  26234  pilem2  26514  pilem3  26515  rlimcnp2  27027  ppisval  27165  ppifi  27167  ppiprm  27212  chtprm  27214  chtdif  27219  efchtdvds  27220  ppidif  27224  ppiltx  27238  prmorcht  27239  ppiub  27266  chtlepsi  27268  pclogsum  27277  vmasum  27278  chpval2  27280  chpub  27282  2sqlem8  27488  chebbnd1lem1  27531  chtppilimlem1  27535  rpvmasum2  27574  dchrisum0re  27575  rplogsum  27589  dirith2  27590  nosupbnd1lem1  27771  nosupbnd2  27779  noinfbnd1lem1  27786  axtgcgrrflx  28488  axtgcgrid  28489  axtgsegcon  28490  axtg5seg  28491  axtgbtwnid  28492  axtgpasch  28493  axtgcont1  28494  phnv  30846  minvecolem2  30907  minvecolem3  30908  minvecolem5  30913  minvecolem6  30914  minvecolem7  30915  hlimcaui  31268  chdmm1i  31509  chabs1  31548  chabs2  31549  ledii  31568  lejdii  31570  pjoml4i  31619  cmbr3i  31632  cmbr4i  31633  cmm1i  31638  osumcor2i  31676  3oalem4  31697  pjssmii  31713  pjocini  31730  pjini  31731  mayete3i  31760  riesz4  32096  riesz1  32097  cnlnadjeui  32109  cnlnadjeu  32110  cnlnssadj  32112  nmopadjlei  32120  pjin1i  32224  pjclem1  32227  stji1i  32274  stm1i  32275  dmdbr2  32335  ssmd1  32343  mdslj2i  32352  mdsl2bi  32355  mdslmd1lem1  32357  mdslmd2i  32362  atomli  32414  atcvat4i  32429  sumdmdlem2  32451  dmdbr5ati  32454  dmdbr6ati  32455  dmdbr7ati  32456  indifbi  32550  disjxpin  32610  imadifxp  32623  nfpconfp  32651  off2  32660  ffsrn  32743  gsummptres  33035  xrge0tsmsd  33041  idlinsubrg  33424  ordtrestNEW  33867  qqhnm  33936  qqhcn  33937  rrhre  33967  indsumin  33986  indf1ofs  33990  esumval  34010  esumel  34011  gsumesum  34023  esumlub  34024  esumcst  34027  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  sigainb  34100  ldgenpisyslem1  34127  measinb2  34187  sibfinima  34304  sibfof  34305  eulerpartlemelr  34322  eulerpartlem1  34332  eulerpartgbij  34337  eulerpartlemgu  34342  eulerpartlemgs2  34345  sseqf  34357  ballotlemfelz  34455  ballotlemfp1  34456  reprinrn  34595  reprinfz1  34599  hgt750lemd  34625  bnj1292  34791  connpconn  35203  iccllysconn  35218  cvmsss2  35242  cvmcov2  35243  cvmopnlem  35246  cvmliftmolem2  35250  cvmliftlem15  35266  cvmlift2lem12  35282  mvrsfpw  35474  msrf  35510  elmsta  35516  mthmpps  35550  nepss  35680  dfon2lem4  35750  txpss3v  35842  fixssdm  35870  fixssrn  35871  limitssson  35875  fneer  36319  neibastop1  36325  neibastop2lem  36326  filnetlem3  36346  ontopbas  36394  bj-disj2r  36994  bj-restpw  37058  bj-discrmoore  37077  bj-idres  37126  bj-fvsnun2  37222  bj-ablssgrp  37242  bj-fldssdrng  37254  taupilemrplb  37286  taupilem2  37288  taupi  37289  ptrest  37579  poimirlem29  37609  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  mbfposadd  37627  sstotbnd2  37734  ssbnd  37748  heibor1lem  37769  heiborlem1  37771  heiborlem3  37773  heiborlem5  37775  heiborlem6  37776  heiborlem10  37780  heibor  37781  opidonOLD  37812  exidcl  37836  flddivrng  37959  iss2  38300  xrnss3v  38328  refrelsredund2  38589  lshpinN  38945  lcvexchlem5  38994  pmodlem2  39804  pmod1i  39805  pmodN  39807  osumcllem7N  39919  pexmidlem4N  39930  pl42lem3N  39938  djaclN  41093  dihoml4c  41333  dochdmj1  41347  djhcl  41357  dochexmidlem4  41420  mapd1o  41605  mapdin  41619  unitscyglem5  42156  elrfi  42650  elrfirn  42651  elrfirn2  42652  ismrcd1  42654  istopclsd  42656  isnacs2  42662  mrefg3  42664  isnacs3  42666  diophrw  42715  diophin  42728  aomclem2  43012  islmodfg  43026  lsmfgcl  43031  lmhmfgima  43041  lmhmfgsplit  43043  lmhmlnmsplit  43044  pwfi2f1o  43053  hbt  43087  ofoafg  43316  harval3  43500  elinintrab  43539  trrelind  43627  clsk3nimkb  44002  isotone2  44011  ismnushort  44270  onfrALTlem2  44517  onfrALTlem2VD  44860  unirestss  45026  inmap  45116  fsumiunss  45496  islptre  45540  sumnnodd  45551  limclner  45572  liminfval4  45710  liminfval3  45711  cnrefiisplem  45750  cncfuni  45807  ismbl3  45907  ismbl4  45914  fouriersw  46152  qndenserrnbllem  46215  salincl  46245  salgencntex  46264  sge0less  46313  sge0resplit  46327  sge0split  46330  sge0iunmptlemre  46336  carageniuncllem1  46442  carageniuncllem2  46443  caragenel2d  46453  hspmbllem3  46549  hspmbl  46550  ovolval2lem  46564  sssmf  46659  smfaddlem1  46684  smflimlem2  46693  smflimlem3  46694  smflimlem4  46695  smfres  46711  smfmullem4  46715  smfsuplem1  46732  fcoreslem2  46979  rngcrescrhmALTV  48003  rhmsubcALTVlem1  48004  funcringcsetcALTV2lem9  48021  fldcALTV  48055  fldhmsubcALTV  48056  iscnrm3llem2  48630  setrec2fun  48784