Theorem inss1 4178

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

Syntax hints:   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  inss2  4179  ssinss1  4187  unabs  4206  nssinpss  4208  dfin4  4219  inv1  4339  disjdif  4413  ifssun  4485  uniintsn  4928  wefrc  5619  relin1  5762  resss  5961  resmpt3  5998  cnvcnvss  6153  resdmss  6194  resssxp  6229  predss  6268  ordtri3or  6350  onfr  6357  ordelinel  6421  funin  6569  funimass2  6576  fnresin1  6618  fnres  6620  fresin  6704  fresaun  6706  nfvres  6873  ssimaex  6920  fneqeql2  6994  fnfvimad  7183  funiunfv  7197  isoini2  7288  ofrfvalg  7633  ofval  7636  ofrval  7637  off  7643  ofres  7644  ofco  7650  fparlem3  8058  fparlem4  8059  frrlem4  8233  frrlem13  8242  smores  8286  smores2  8288  tfrlem5  8313  pmresg  8812  sbthlem7  9025  sbthcl  9031  infi  9174  imafi  9219  ixpfi2  9254  unifpw  9259  elfiun  9337  dffi3  9338  marypha1lem  9340  ordtypelem6  9432  ordtypelem7  9433  ordtypelem8  9434  wdomima2g  9495  frmin  9667  frrlem15  9675  frrlem16  9676  tskwe  9868  ackbij1lem15  10149  ackbij1lem16  10150  fin23lem23  10242  fin23lem22  10243  fin23lem19  10252  brdom3  10444  brdom5  10445  brdom4  10446  imadomg  10450  fpwwe2lem11  10558  canthp1lem2  10570  wunin  10630  tskin  10676  gruima  10719  ingru  10732  gruina  10735  grur1a  10736  nqerf  10847  nqerrel  10849  hashun3  14340  hashin  14367  hashdif  14369  xptrrel  14936  rexanuz  15302  limsupgle  15433  rlimres  15514  lo1res  15515  lo1resb  15520  rlimresb  15521  o1resb  15522  lo1eq  15524  rlimeq  15525  o1of2  15569  o1rlimmul  15575  isercolllem2  15622  isercolllem3  15623  isercoll  15624  incexclem  15795  incexc  15796  bitsinvp1  16412  sadcaddlem  16420  sadadd2lem  16422  sadadd3  16424  sadaddlem  16429  sadasslem  16433  sadeq  16435  bitsres  16436  smuval2  16445  smupval  16451  smueqlem  16453  smumul  16456  ramub2  16979  ramub1lem2  16992  fvsetsid  17132  ressbasss2  17205  ressinbas  17209  ressress  17211  submre  17561  isacs1i  17617  mreacs  17618  acsfn  17619  invss  17722  sscres  17784  catcisolem  18071  catciso  18072  isacs5lem  18505  psss  18540  tsrss  18549  tsrdir  18564  sylow2a  19588  lsmmod  19644  gsumzres  19878  gsumzaddlem  19890  dprddisj2  20010  ablfac1eu  20044  isunit  20347  rngcbas  20592  rngchomfval  20593  rngccofval  20597  dfrngc2  20599  rnghmsscmap2  20600  rnghmsscmap  20601  rngcsect  20607  funcrngcsetc  20611  ringcbas  20621  ringchomfval  20622  ringccofval  20626  dfringc2  20628  rhmsscmap2  20629  rhmsscmap  20630  rhmsscrnghm  20636  ringcsect  20641  funcringcsetc  20645  rngcrescrhm  20655  rhmsubclem1  20656  fldc  20755  fldhmsubc  20756  acsfn1p  20770  lspextmo  21046  2idlval  21244  pjfval  21699  pjpm  21701  aspsubrg  21868  psrbagsn  22054  ofco2  22429  basdif0  22931  tgval2  22934  eltg3  22940  tgcl  22947  tgdom  22956  tgidm  22958  ppttop  22985  epttop  22987  ntropn  23027  ntrin  23039  mretopd  23070  neiptoptop  23109  restfpw  23157  neitr  23158  restcls  23159  cncls  23252  cnpresti  23266  cnprest  23267  cmpsublem  23377  cmpsub  23378  fiuncmp  23382  indisconn  23396  connsub  23399  iunconnlem  23405  islly2  23462  cldllycmp  23473  kgentopon  23516  ptbasfi  23559  ptcnplem  23599  txcnmpt  23602  txcmplem2  23620  hausdiag  23623  txkgen  23630  xkococnlem  23637  qtoptop2  23677  basqtop  23689  fbssfi  23815  filin  23832  infil  23841  fbasrn  23862  fgtr  23868  ufprim  23887  flimrest  23961  txflf  23984  fclsrest  24002  alexsubALTlem4  24028  tsmsres  24122  tsmsxplem1  24131  ustund  24200  trust  24207  utoptop  24212  restutop  24215  cfiluweak  24272  xmetres  24342  metres  24343  blin2  24407  setsmstopn  24456  metrest  24502  ressxms  24503  tgioo  24774  xrsmopn  24791  reconnlem1  24805  xrge0tsms  24813  tcphcph  25217  cfilresi  25275  cfilres  25276  caussi  25277  causs  25278  relcmpcmet  25298  minveclem4a  25410  ismbl2  25507  cmmbl  25514  nulmbl2  25516  unmbl  25517  shftmbl  25518  volinun  25526  voliunlem1  25530  voliunlem2  25531  ioombl1lem4  25541  ioombl1  25542  uniioombllem2  25563  uniioombllem3  25565  uniioombllem4  25566  uniioombllem5  25567  uniioombl  25569  volivth  25587  vitalilem3  25590  vitalilem4  25591  vitalilem5  25592  vitali  25593  mbfadd  25641  mbfsub  25642  i1fadd  25675  itg1addlem2  25677  itg1addlem4  25679  itg1addlem5  25680  itg1climres  25694  mbfmul  25706  itg2splitlem  25728  itg2split  25729  limcresi  25865  limciun  25874  dvreslem  25889  dvres2lem  25890  dvres  25891  dvres3a  25894  dvaddbr  25918  dvmulbr  25919  dvfsumle  26001  dvfsumabs  26003  ig1peu  26153  pilem2  26433  pilem3  26434  rlimcnp2  26946  ppisval  27084  ppifi  27086  ppiprm  27131  chtprm  27133  chtdif  27138  efchtdvds  27139  ppidif  27143  ppiltx  27157  prmorcht  27158  ppiub  27184  chtlepsi  27186  pclogsum  27195  vmasum  27196  chpval2  27198  chpub  27200  2sqlem8  27406  chebbnd1lem1  27449  chtppilimlem1  27453  rpvmasum2  27492  dchrisum0re  27493  rplogsum  27507  dirith2  27508  nosupbnd1lem1  27689  nosupbnd2  27697  noinfbnd1lem1  27704  axtgcgrrflx  28547  axtgcgrid  28548  axtgsegcon  28549  axtg5seg  28550  axtgbtwnid  28551  axtgpasch  28552  axtgcont1  28553  phnv  30903  minvecolem2  30964  minvecolem3  30965  minvecolem5  30970  minvecolem6  30971  minvecolem7  30972  hlimcaui  31325  chdmm1i  31566  chabs1  31605  chabs2  31606  ledii  31625  lejdii  31627  pjoml4i  31676  cmbr3i  31689  cmbr4i  31690  cmm1i  31695  osumcor2i  31733  3oalem4  31754  pjssmii  31770  pjocini  31787  pjini  31788  mayete3i  31817  riesz4  32153  riesz1  32154  cnlnadjeui  32166  cnlnadjeu  32167  cnlnssadj  32169  nmopadjlei  32177  pjin1i  32281  pjclem1  32284  stji1i  32331  stm1i  32332  dmdbr2  32392  ssmd1  32400  mdslj2i  32409  mdsl2bi  32412  mdslmd1lem1  32414  mdslmd2i  32419  atomli  32471  atcvat4i  32486  sumdmdlem2  32508  dmdbr5ati  32511  dmdbr6ati  32512  dmdbr7ati  32513  indifbi  32608  disjxpin  32676  imadifxp  32689  nfpconfp  32723  off2  32732  ffsrn  32819  indsumin  32939  indf1ofs  32944  gsummptres  33131  xrge0tsmsd  33152  idlinsubrg  33509  ordtrestNEW  34084  qqhnm  34153  qqhcn  34154  rrhre  34184  esumval  34209  esumel  34210  gsumesum  34222  esumlub  34223  esumcst  34226  esumfsup  34233  esumpcvgval  34241  esumcvg  34249  sigainb  34299  ldgenpisyslem1  34326  measinb2  34386  sibfinima  34502  sibfof  34503  eulerpartlemelr  34520  eulerpartlem1  34530  eulerpartgbij  34535  eulerpartlemgu  34540  eulerpartlemgs2  34543  sseqf  34555  ballotlemfelz  34654  ballotlemfp1  34655  reprinrn  34781  reprinfz1  34785  hgt750lemd  34811  bnj1292  34976  connpconn  35436  iccllysconn  35451  cvmsss2  35475  cvmcov2  35476  cvmopnlem  35479  cvmliftmolem2  35483  cvmliftlem15  35499  cvmlift2lem12  35515  mvrsfpw  35707  msrf  35743  elmsta  35749  mthmpps  35783  nepss  35919  dfon2lem4  35985  txpss3v  36077  fixssdm  36105  fixssrn  36106  limitssson  36110  fneer  36554  neibastop1  36560  neibastop2lem  36561  filnetlem3  36581  ontopbas  36629  bj-disj2r  37354  bj-restpw  37423  bj-discrmoore  37442  bj-idres  37493  bj-fvsnun2  37589  bj-ablssgrp  37609  bj-fldssdrng  37621  taupilemrplb  37653  taupilem2  37655  taupi  37656  ptrest  37957  poimirlem29  37987  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  mbfposadd  38005  sstotbnd2  38112  ssbnd  38126  heibor1lem  38147  heiborlem1  38149  heiborlem3  38151  heiborlem5  38153  heiborlem6  38154  heiborlem10  38158  heibor  38159  opidonOLD  38190  exidcl  38214  flddivrng  38337  iss2  38682  xrnss3v  38719  refrelsredund2  39055  lshpinN  39452  lcvexchlem5  39501  pmodlem2  40310  pmod1i  40311  pmodN  40313  osumcllem7N  40425  pexmidlem4N  40436  pl42lem3N  40444  djaclN  41599  dihoml4c  41839  dochdmj1  41853  djhcl  41863  dochexmidlem4  41926  mapd1o  42111  mapdin  42125  unitscyglem5  42655  redvmptabs  42809  elrfi  43143  elrfirn  43144  elrfirn2  43145  ismrcd1  43147  istopclsd  43149  isnacs2  43155  mrefg3  43157  isnacs3  43159  diophrw  43208  diophin  43221  aomclem2  43504  islmodfg  43518  lsmfgcl  43523  lmhmfgima  43533  lmhmfgsplit  43535  lmhmlnmsplit  43536  pwfi2f1o  43545  hbt  43579  ofoafg  43803  harval3  43986  elinintrab  44025  trrelind  44113  clsk3nimkb  44488  isotone2  44497  ismnushort  44749  onfrALTlem2  44994  onfrALTlem2VD  45336  wfac8prim  45450  unirestss  45575  inmap  45659  fsumiunss  46026  islptre  46070  sumnnodd  46081  limclner  46100  liminfval4  46238  liminfval3  46239  cnrefiisplem  46278  cncfuni  46335  ismbl3  46435  ismbl4  46442  fouriersw  46680  qndenserrnbllem  46743  salincl  46773  salgencntex  46792  sge0less  46841  sge0resplit  46855  sge0split  46858  sge0iunmptlemre  46864  carageniuncllem1  46970  carageniuncllem2  46971  caragenel2d  46981  hspmbllem3  47077  hspmbl  47078  ovolval2lem  47092  sssmf  47187  smfaddlem1  47212  smflimlem2  47221  smflimlem3  47222  smflimlem4  47223  smfres  47239  smfmullem4  47243  smfsuplem1  47260  fcoreslem2  47527  indprmfz  48108  ppivalnn  48110  rngcrescrhmALTV  48771  rhmsubcALTVlem1  48772  funcringcsetcALTV2lem9  48789  fldcALTV  48823  fldhmsubcALTV  48824  iscnrm3llem2  49440  uptrlem1  49700  uptrlem2  49701  uptrlem3  49702  uptra  49705  uptrar  49706  uobeqw  49709  uptr2  49711  uptr2a  49712  fucoppcfunc  49902  setrec2fun  50182