Theorem inss1 4227

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

Syntax hints:   ∩ cin 3946   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954  df-ss 3964

This theorem is referenced by:  inss2  4228  ssinss1  4236  unabs  4253  nssinpss  4255  dfin4  4266  inv1  4393  disjdif  4470  ifssun  4544  uniintsn  4990  wefrc  5669  relin1  5810  resss  6004  resmpt3  6036  cnvcnvss  6190  resdmss  6231  resssxp  6266  predss  6305  ordtri3or  6393  onfr  6400  ordelinel  6462  funin  6621  funimass2  6628  fnresin1  6672  fnres  6674  fresin  6757  fresaun  6759  nfvres  6929  ssimaex  6972  fneqeql2  7044  fnfvimad  7231  funiunfv  7242  isoini2  7331  ofrfvalg  7673  ofval  7676  ofrval  7677  off  7683  ofres  7684  ofco  7688  fparlem3  8095  fparlem4  8096  frrlem4  8269  frrlem13  8278  smores  8347  smores2  8349  tfrlem5  8375  pmresg  8860  sbthlem7  9085  sbthcl  9091  infi  9264  imafiALT  9341  ixpfi2  9346  unifpw  9351  elfiun  9421  dffi3  9422  marypha1lem  9424  ordtypelem6  9514  ordtypelem7  9515  ordtypelem8  9516  wdomima2g  9577  frmin  9740  frrlem15  9748  frrlem16  9749  tskwe  9941  ackbij1lem15  10225  ackbij1lem16  10226  fin23lem23  10317  fin23lem22  10318  fin23lem19  10327  brdom3  10519  brdom5  10520  brdom4  10521  imadomg  10525  fpwwe2lem11  10632  canthp1lem2  10644  wunin  10704  tskin  10750  gruima  10793  ingru  10806  gruina  10809  grur1a  10810  nqerf  10921  nqerrel  10923  hashun3  14340  hashin  14367  hashdif  14369  xptrrel  14923  rexanuz  15288  limsupgle  15417  rlimres  15498  lo1res  15499  lo1resb  15504  rlimresb  15505  o1resb  15506  lo1eq  15508  rlimeq  15509  o1of2  15553  o1rlimmul  15559  isercolllem2  15608  isercolllem3  15609  isercoll  15610  incexclem  15778  incexc  15779  bitsinvp1  16386  sadcaddlem  16394  sadadd2lem  16396  sadadd3  16398  sadaddlem  16403  sadasslem  16407  sadeq  16409  bitsres  16410  smuval2  16419  smupval  16425  smueqlem  16427  smumul  16430  ramub2  16943  ramub1lem2  16956  fvsetsid  17097  ressbasss2  17181  ressinbas  17186  ressress  17189  submre  17545  isacs1i  17597  mreacs  17598  acsfn  17599  invss  17704  sscres  17766  catcisolem  18056  catciso  18057  isacs5lem  18494  psss  18529  tsrss  18538  tsrdir  18553  sylow2a  19480  lsmmod  19536  gsumzres  19769  gsumzaddlem  19781  dprddisj2  19901  ablfac1eu  19935  isunit  20176  acsfn1p  20403  lspextmo  20655  2idlval  20845  pjfval  21245  pjpm  21247  aspsubrg  21412  psrbagsn  21606  ofco2  21935  basdif0  22438  tgval2  22441  eltg3  22447  tgcl  22454  tgdom  22463  tgidm  22465  ppttop  22492  epttop  22494  ntropn  22535  ntrin  22547  mretopd  22578  neiptoptop  22617  restfpw  22665  neitr  22666  restcls  22667  cncls  22760  cnpresti  22774  cnprest  22775  cmpsublem  22885  cmpsub  22886  fiuncmp  22890  indisconn  22904  connsub  22907  iunconnlem  22913  islly2  22970  cldllycmp  22981  kgentopon  23024  ptbasfi  23067  ptcnplem  23107  txcnmpt  23110  txcmplem2  23128  hausdiag  23131  txkgen  23138  xkococnlem  23145  qtoptop2  23185  basqtop  23197  fbssfi  23323  filin  23340  infil  23349  fbasrn  23370  fgtr  23376  ufprim  23395  flimrest  23469  txflf  23492  fclsrest  23510  alexsubALTlem4  23536  tsmsres  23630  tsmsxplem1  23639  ustund  23708  trust  23716  utoptop  23721  restutop  23724  cfiluweak  23782  xmetres  23852  metres  23853  blin2  23917  setsmstopn  23968  metrest  24015  ressxms  24016  tgioo  24294  xrsmopn  24310  reconnlem1  24324  xrge0tsms  24332  tcphcph  24736  cfilresi  24794  cfilres  24795  caussi  24796  causs  24797  relcmpcmet  24817  minveclem4a  24929  ismbl2  25026  cmmbl  25033  nulmbl2  25035  unmbl  25036  shftmbl  25037  volinun  25045  voliunlem1  25049  voliunlem2  25050  ioombl1lem4  25060  ioombl1  25061  uniioombllem2  25082  uniioombllem3  25084  uniioombllem4  25085  uniioombllem5  25086  uniioombl  25088  volivth  25106  vitalilem3  25109  vitalilem4  25110  vitalilem5  25111  vitali  25112  mbfadd  25160  mbfsub  25161  i1fadd  25194  itg1addlem2  25196  itg1addlem4  25198  itg1addlem4OLD  25199  itg1addlem5  25200  itg1climres  25214  mbfmul  25226  itg2splitlem  25248  itg2split  25249  limcresi  25384  limciun  25393  dvreslem  25408  dvres2lem  25409  dvres  25410  dvres3a  25413  dvaddbr  25437  dvmulbr  25438  dvfsumle  25520  dvfsumabs  25522  ig1peu  25671  pilem2  25946  pilem3  25947  rlimcnp2  26451  ppisval  26588  ppifi  26590  ppiprm  26635  chtprm  26637  chtdif  26642  efchtdvds  26643  ppidif  26647  ppiltx  26661  prmorcht  26662  ppiub  26687  chtlepsi  26689  pclogsum  26698  vmasum  26699  chpval2  26701  chpub  26703  2sqlem8  26909  chebbnd1lem1  26952  chtppilimlem1  26956  rpvmasum2  26995  dchrisum0re  26996  rplogsum  27010  dirith2  27011  nosupbnd1lem1  27191  nosupbnd2  27199  noinfbnd1lem1  27206  axtgcgrrflx  27693  axtgcgrid  27694  axtgsegcon  27695  axtg5seg  27696  axtgbtwnid  27697  axtgpasch  27698  axtgcont1  27699  phnv  30045  minvecolem2  30106  minvecolem3  30107  minvecolem5  30112  minvecolem6  30113  minvecolem7  30114  hlimcaui  30467  chdmm1i  30708  chabs1  30747  chabs2  30748  ledii  30767  lejdii  30769  pjoml4i  30818  cmbr3i  30831  cmbr4i  30832  cmm1i  30837  osumcor2i  30875  3oalem4  30896  pjssmii  30912  pjocini  30929  pjini  30930  mayete3i  30959  riesz4  31295  riesz1  31296  cnlnadjeui  31308  cnlnadjeu  31309  cnlnssadj  31311  nmopadjlei  31319  pjin1i  31423  pjclem1  31426  stji1i  31473  stm1i  31474  dmdbr2  31534  ssmd1  31542  mdslj2i  31551  mdsl2bi  31554  mdslmd1lem1  31556  mdslmd2i  31561  atomli  31613  atcvat4i  31628  sumdmdlem2  31650  dmdbr5ati  31653  dmdbr6ati  31654  dmdbr7ati  31655  indifbi  31736  disjxpin  31797  imadifxp  31810  nfpconfp  31834  off2  31844  ffsrn  31932  gsummptres  32182  xrge0tsmsd  32187  idlinsubrg  32507  ordtrestNEW  32839  qqhnm  32908  qqhcn  32909  rrhre  32939  indsumin  32958  indf1ofs  32962  esumval  32982  esumel  32983  gsumesum  32995  esumlub  32996  esumcst  32999  esumfsup  33006  esumpcvgval  33014  esumcvg  33022  sigainb  33072  ldgenpisyslem1  33099  measinb2  33159  sibfinima  33276  sibfof  33277  eulerpartlemelr  33294  eulerpartlem1  33304  eulerpartgbij  33309  eulerpartlemgu  33314  eulerpartlemgs2  33317  sseqf  33329  ballotlemfelz  33427  ballotlemfp1  33428  reprinrn  33568  reprinfz1  33572  hgt750lemd  33598  bnj1292  33764  connpconn  34164  iccllysconn  34179  cvmsss2  34203  cvmcov2  34204  cvmopnlem  34207  cvmliftmolem2  34211  cvmliftlem15  34227  cvmlift2lem12  34243  mvrsfpw  34435  msrf  34471  elmsta  34477  mthmpps  34511  nepss  34625  dfon2lem4  34696  txpss3v  34788  fixssdm  34816  fixssrn  34817  limitssson  34821  gg-dvmulbr  35113  gg-dvfsumle  35120  fneer  35176  neibastop1  35182  neibastop2lem  35183  filnetlem3  35203  ontopbas  35251  bj-disj2r  35847  bj-restpw  35911  bj-discrmoore  35930  bj-idres  35979  bj-fvsnun2  36075  bj-ablssgrp  36095  bj-fldssdrng  36107  taupilemrplb  36139  taupilem2  36141  taupi  36142  ptrest  36425  poimirlem29  36455  mblfinlem3  36465  mblfinlem4  36466  ismblfin  36467  mbfposadd  36473  sstotbnd2  36580  ssbnd  36594  heibor1lem  36615  heiborlem1  36617  heiborlem3  36619  heiborlem5  36621  heiborlem6  36622  heiborlem10  36626  heibor  36627  opidonOLD  36658  exidcl  36682  flddivrng  36805  iss2  37151  xrnss3v  37180  refrelsredund2  37441  lshpinN  37797  lcvexchlem5  37846  pmodlem2  38656  pmod1i  38657  pmodN  38659  osumcllem7N  38771  pexmidlem4N  38782  pl42lem3N  38790  djaclN  39945  dihoml4c  40185  dochdmj1  40199  djhcl  40209  dochexmidlem4  40272  mapd1o  40457  mapdin  40471  elrfi  41365  elrfirn  41366  elrfirn2  41367  ismrcd1  41369  istopclsd  41371  isnacs2  41377  mrefg3  41379  isnacs3  41381  diophrw  41430  diophin  41443  aomclem2  41730  islmodfg  41744  lsmfgcl  41749  lmhmfgima  41759  lmhmfgsplit  41761  lmhmlnmsplit  41762  pwfi2f1o  41771  hbt  41805  ofoafg  42037  harval3  42222  elinintrab  42261  trrelind  42349  clsk3nimkb  42724  isotone2  42733  ismnushort  42993  onfrALTlem2  43240  onfrALTlem2VD  43583  unirestss  43746  inmap  43841  fsumiunss  44226  islptre  44270  sumnnodd  44281  limclner  44302  liminfval4  44440  liminfval3  44441  cnrefiisplem  44480  cncfuni  44537  ismbl3  44637  ismbl4  44644  fouriersw  44882  qndenserrnbllem  44945  salincl  44975  salgencntex  44994  sge0less  45043  sge0resplit  45057  sge0split  45060  sge0iunmptlemre  45066  carageniuncllem1  45172  carageniuncllem2  45173  caragenel2d  45183  hspmbllem3  45279  hspmbl  45280  ovolval2lem  45294  sssmf  45389  smfaddlem1  45414  smflimlem2  45423  smflimlem3  45424  smflimlem4  45425  smfres  45441  smfmullem4  45445  smfsuplem1  45462  fcoreslem2  45709  rngcbas  46765  rngchomfval  46766  rngccofval  46770  dfrngc2  46772  rnghmsscmap2  46773  rnghmsscmap  46774  rngcsect  46780  funcrngcsetc  46798  ringcbas  46811  ringchomfval  46812  ringccofval  46816  dfringc2  46818  rhmsscmap2  46819  rhmsscmap  46820  rhmsscrnghm  46826  ringcsect  46831  funcringcsetc  46835  funcringcsetcALTV2lem9  46844  fldc  46883  fldhmsubc  46884  rngcrescrhm  46885  rhmsubclem1  46886  fldcALTV  46901  fldhmsubcALTV  46902  rngcrescrhmALTV  46903  rhmsubcALTVlem1  46904  iscnrm3llem2  47485  setrec2fun  47639