Theorem inss1 4200

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

Syntax hints:   ∩ cin 3913   ⊆ wss 3914

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  inss2  4201  ssinss1  4209  unabs  4228  nssinpss  4230  dfin4  4241  inv1  4361  disjdif  4435  ifssun  4506  uniintsn  4949  wefrc  5632  relin1  5775  resss  5972  resmpt3  6009  cnvcnvss  6167  resdmss  6208  resssxp  6243  predss  6282  ordtri3or  6364  onfr  6371  ordelinel  6435  funin  6592  funimass2  6599  fnresin1  6643  fnres  6645  fresin  6729  fresaun  6731  nfvres  6899  ssimaex  6946  fneqeql2  7019  fnfvimad  7208  funiunfv  7222  isoini2  7314  ofrfvalg  7661  ofval  7664  ofrval  7665  off  7671  ofres  7672  ofco  7678  fparlem3  8093  fparlem4  8094  frrlem4  8268  frrlem13  8277  smores  8321  smores2  8323  tfrlem5  8348  pmresg  8843  sbthlem7  9057  sbthcl  9063  infi  9213  imafi  9264  ixpfi2  9301  unifpw  9306  elfiun  9381  dffi3  9382  marypha1lem  9384  ordtypelem6  9476  ordtypelem7  9477  ordtypelem8  9478  wdomima2g  9539  frmin  9702  frrlem15  9710  frrlem16  9711  tskwe  9903  ackbij1lem15  10186  ackbij1lem16  10187  fin23lem23  10279  fin23lem22  10280  fin23lem19  10289  brdom3  10481  brdom5  10482  brdom4  10483  imadomg  10487  fpwwe2lem11  10594  canthp1lem2  10606  wunin  10666  tskin  10712  gruima  10755  ingru  10768  gruina  10771  grur1a  10772  nqerf  10883  nqerrel  10885  hashun3  14349  hashin  14376  hashdif  14378  xptrrel  14946  rexanuz  15312  limsupgle  15443  rlimres  15524  lo1res  15525  lo1resb  15530  rlimresb  15531  o1resb  15532  lo1eq  15534  rlimeq  15535  o1of2  15579  o1rlimmul  15585  isercolllem2  15632  isercolllem3  15633  isercoll  15634  incexclem  15802  incexc  15803  bitsinvp1  16419  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  sadeq  16442  bitsres  16443  smuval2  16452  smupval  16458  smueqlem  16460  smumul  16463  ramub2  16985  ramub1lem2  16998  fvsetsid  17138  ressbasss2  17211  ressinbas  17215  ressress  17217  submre  17566  isacs1i  17618  mreacs  17619  acsfn  17620  invss  17723  sscres  17785  catcisolem  18072  catciso  18073  isacs5lem  18504  psss  18539  tsrss  18548  tsrdir  18563  sylow2a  19549  lsmmod  19605  gsumzres  19839  gsumzaddlem  19851  dprddisj2  19971  ablfac1eu  20005  isunit  20282  rngcbas  20530  rngchomfval  20531  rngccofval  20535  dfrngc2  20537  rnghmsscmap2  20538  rnghmsscmap  20539  rngcsect  20545  funcrngcsetc  20549  ringcbas  20559  ringchomfval  20560  ringccofval  20564  dfringc2  20566  rhmsscmap2  20567  rhmsscmap  20568  rhmsscrnghm  20574  ringcsect  20579  funcringcsetc  20583  rngcrescrhm  20593  rhmsubclem1  20594  fldc  20693  fldhmsubc  20694  acsfn1p  20708  lspextmo  20963  2idlval  21161  pjfval  21615  pjpm  21617  aspsubrg  21785  psrbagsn  21970  ofco2  22338  basdif0  22840  tgval2  22843  eltg3  22849  tgcl  22856  tgdom  22865  tgidm  22867  ppttop  22894  epttop  22896  ntropn  22936  ntrin  22948  mretopd  22979  neiptoptop  23018  restfpw  23066  neitr  23067  restcls  23068  cncls  23161  cnpresti  23175  cnprest  23176  cmpsublem  23286  cmpsub  23287  fiuncmp  23291  indisconn  23305  connsub  23308  iunconnlem  23314  islly2  23371  cldllycmp  23382  kgentopon  23425  ptbasfi  23468  ptcnplem  23508  txcnmpt  23511  txcmplem2  23529  hausdiag  23532  txkgen  23539  xkococnlem  23546  qtoptop2  23586  basqtop  23598  fbssfi  23724  filin  23741  infil  23750  fbasrn  23771  fgtr  23777  ufprim  23796  flimrest  23870  txflf  23893  fclsrest  23911  alexsubALTlem4  23937  tsmsres  24031  tsmsxplem1  24040  ustund  24109  trust  24117  utoptop  24122  restutop  24125  cfiluweak  24182  xmetres  24252  metres  24253  blin2  24317  setsmstopn  24366  metrest  24412  ressxms  24413  tgioo  24684  xrsmopn  24701  reconnlem1  24715  xrge0tsms  24723  tcphcph  25137  cfilresi  25195  cfilres  25196  caussi  25197  causs  25198  relcmpcmet  25218  minveclem4a  25330  ismbl2  25428  cmmbl  25435  nulmbl2  25437  unmbl  25438  shftmbl  25439  volinun  25447  voliunlem1  25451  voliunlem2  25452  ioombl1lem4  25462  ioombl1  25463  uniioombllem2  25484  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombl  25490  volivth  25508  vitalilem3  25511  vitalilem4  25512  vitalilem5  25513  vitali  25514  mbfadd  25562  mbfsub  25563  i1fadd  25596  itg1addlem2  25598  itg1addlem4  25600  itg1addlem5  25601  itg1climres  25615  mbfmul  25627  itg2splitlem  25649  itg2split  25650  limcresi  25786  limciun  25795  dvreslem  25810  dvres2lem  25811  dvres  25812  dvres3a  25815  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  ig1peu  26080  pilem2  26362  pilem3  26363  rlimcnp2  26876  ppisval  27014  ppifi  27016  ppiprm  27061  chtprm  27063  chtdif  27068  efchtdvds  27069  ppidif  27073  ppiltx  27087  prmorcht  27088  ppiub  27115  chtlepsi  27117  pclogsum  27126  vmasum  27127  chpval2  27129  chpub  27131  2sqlem8  27337  chebbnd1lem1  27380  chtppilimlem1  27384  rpvmasum2  27423  dchrisum0re  27424  rplogsum  27438  dirith2  27439  nosupbnd1lem1  27620  nosupbnd2  27628  noinfbnd1lem1  27635  axtgcgrrflx  28389  axtgcgrid  28390  axtgsegcon  28391  axtg5seg  28392  axtgbtwnid  28393  axtgpasch  28394  axtgcont1  28395  phnv  30743  minvecolem2  30804  minvecolem3  30805  minvecolem5  30810  minvecolem6  30811  minvecolem7  30812  hlimcaui  31165  chdmm1i  31406  chabs1  31445  chabs2  31446  ledii  31465  lejdii  31467  pjoml4i  31516  cmbr3i  31529  cmbr4i  31530  cmm1i  31535  osumcor2i  31573  3oalem4  31594  pjssmii  31610  pjocini  31627  pjini  31628  mayete3i  31657  riesz4  31993  riesz1  31994  cnlnadjeui  32006  cnlnadjeu  32007  cnlnssadj  32009  nmopadjlei  32017  pjin1i  32121  pjclem1  32124  stji1i  32171  stm1i  32172  dmdbr2  32232  ssmd1  32240  mdslj2i  32249  mdsl2bi  32252  mdslmd1lem1  32254  mdslmd2i  32259  atomli  32311  atcvat4i  32326  sumdmdlem2  32348  dmdbr5ati  32351  dmdbr6ati  32352  dmdbr7ati  32353  indifbi  32449  disjxpin  32517  imadifxp  32530  nfpconfp  32556  off2  32565  ffsrn  32652  indsumin  32785  indf1ofs  32789  gsummptres  32992  xrge0tsmsd  33002  idlinsubrg  33402  ordtrestNEW  33911  qqhnm  33980  qqhcn  33981  rrhre  34011  esumval  34036  esumel  34037  gsumesum  34049  esumlub  34050  esumcst  34053  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  sigainb  34126  ldgenpisyslem1  34153  measinb2  34213  sibfinima  34330  sibfof  34331  eulerpartlemelr  34348  eulerpartlem1  34358  eulerpartgbij  34363  eulerpartlemgu  34368  eulerpartlemgs2  34371  sseqf  34383  ballotlemfelz  34482  ballotlemfp1  34483  reprinrn  34609  reprinfz1  34613  hgt750lemd  34639  bnj1292  34805  connpconn  35222  iccllysconn  35237  cvmsss2  35261  cvmcov2  35262  cvmopnlem  35265  cvmliftmolem2  35269  cvmliftlem15  35285  cvmlift2lem12  35301  mvrsfpw  35493  msrf  35529  elmsta  35535  mthmpps  35569  nepss  35705  dfon2lem4  35774  txpss3v  35866  fixssdm  35894  fixssrn  35895  limitssson  35899  fneer  36341  neibastop1  36347  neibastop2lem  36348  filnetlem3  36368  ontopbas  36416  bj-disj2r  37016  bj-restpw  37080  bj-discrmoore  37099  bj-idres  37148  bj-fvsnun2  37244  bj-ablssgrp  37264  bj-fldssdrng  37276  taupilemrplb  37308  taupilem2  37310  taupi  37311  ptrest  37613  poimirlem29  37643  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  mbfposadd  37661  sstotbnd2  37768  ssbnd  37782  heibor1lem  37803  heiborlem1  37805  heiborlem3  37807  heiborlem5  37809  heiborlem6  37810  heiborlem10  37814  heibor  37815  opidonOLD  37846  exidcl  37870  flddivrng  37993  iss2  38326  xrnss3v  38354  refrelsredund2  38624  lshpinN  38982  lcvexchlem5  39031  pmodlem2  39841  pmod1i  39842  pmodN  39844  osumcllem7N  39956  pexmidlem4N  39967  pl42lem3N  39975  djaclN  41130  dihoml4c  41370  dochdmj1  41384  djhcl  41394  dochexmidlem4  41457  mapd1o  41642  mapdin  41656  unitscyglem5  42187  redvmptabs  42348  elrfi  42682  elrfirn  42683  elrfirn2  42684  ismrcd1  42686  istopclsd  42688  isnacs2  42694  mrefg3  42696  isnacs3  42698  diophrw  42747  diophin  42760  aomclem2  43044  islmodfg  43058  lsmfgcl  43063  lmhmfgima  43073  lmhmfgsplit  43075  lmhmlnmsplit  43076  pwfi2f1o  43085  hbt  43119  ofoafg  43343  harval3  43527  elinintrab  43566  trrelind  43654  clsk3nimkb  44029  isotone2  44038  ismnushort  44290  onfrALTlem2  44536  onfrALTlem2VD  44878  wfac8prim  44992  unirestss  45118  inmap  45203  fsumiunss  45573  islptre  45617  sumnnodd  45628  limclner  45649  liminfval4  45787  liminfval3  45788  cnrefiisplem  45827  cncfuni  45884  ismbl3  45984  ismbl4  45991  fouriersw  46229  qndenserrnbllem  46292  salincl  46322  salgencntex  46341  sge0less  46390  sge0resplit  46404  sge0split  46407  sge0iunmptlemre  46413  carageniuncllem1  46519  carageniuncllem2  46520  caragenel2d  46530  hspmbllem3  46626  hspmbl  46627  ovolval2lem  46641  sssmf  46736  smfaddlem1  46761  smflimlem2  46770  smflimlem3  46771  smflimlem4  46772  smfres  46788  smfmullem4  46792  smfsuplem1  46809  fcoreslem2  47065  rngcrescrhmALTV  48268  rhmsubcALTVlem1  48269  funcringcsetcALTV2lem9  48286  fldcALTV  48320  fldhmsubcALTV  48321  iscnrm3llem2  48938  uptrlem1  49199  uptrlem2  49200  uptrlem3  49201  uptra  49204  uptrar  49205  uobeqw  49208  uptr2  49210  uptr2a  49211  fucoppcfunc  49401  setrec2fun  49681