Theorem inss1 4205

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

Syntax hints:   ∩ cin 3935   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  inss2  4206  ssinss1  4214  unabs  4231  nssinpss  4233  dfin4  4244  inv1  4348  disjdif  4421  uniintsn  4913  wefrc  5549  relin1  5685  resss  5878  resmpt3  5906  cnvcnvss  6051  predss  6155  ordtri3or  6223  onfr  6230  ordelinel  6289  funin  6430  funimass2  6437  fnresin1  6472  fnres  6474  fresin  6547  fresaun  6549  nfvres  6706  ssimaex  6748  fneqeql2  6817  fnfvimad  6996  funiunfv  7007  isoini2  7092  ofrfval  7417  ofval  7418  ofrval  7419  off  7424  ofres  7425  ofco  7429  fparlem3  7809  fparlem4  7810  smores  7989  smores2  7991  tfrlem5  8016  pmresg  8434  sbthlem7  8633  sbthcl  8639  infi  8742  imafi  8817  ixpfi2  8822  unifpw  8827  elfiun  8894  dffi3  8895  marypha1lem  8897  ordtypelem6  8987  ordtypelem7  8988  ordtypelem8  8989  wdomima2g  9050  tskwe  9379  ackbij1lem15  9656  ackbij1lem16  9657  fin23lem23  9748  fin23lem22  9749  fin23lem19  9758  brdom3  9950  brdom5  9951  brdom4  9952  imadomg  9956  fpwwe2lem12  10063  canthp1lem2  10075  wunin  10135  tskin  10181  gruima  10224  ingru  10237  gruina  10240  grur1a  10241  nqerf  10352  nqerrel  10354  hashun3  13746  hashin  13773  hashdif  13775  xptrrel  14340  rexanuz  14705  limsupgle  14834  rlimres  14915  lo1res  14916  lo1resb  14921  rlimresb  14922  o1resb  14923  lo1eq  14925  rlimeq  14926  o1of2  14969  o1rlimmul  14975  isercolllem2  15022  isercolllem3  15023  isercoll  15024  incexclem  15191  incexc  15192  bitsinvp1  15798  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  sadasslem  15819  sadeq  15821  bitsres  15822  smuval2  15831  smupval  15837  smueqlem  15839  smumul  15842  ramub2  16350  ramub1lem2  16363  fvsetsid  16515  ressinbas  16560  ressress  16562  submre  16876  isacs1i  16928  mreacs  16929  acsfn  16930  invss  17031  sscres  17093  catcisolem  17366  catciso  17367  isacs5lem  17779  psss  17824  tsrss  17833  tsrdir  17848  sylow2a  18744  lsmmod  18801  gsumzres  19029  gsumzaddlem  19041  dprddisj2  19161  ablfac1eu  19195  isunit  19407  acsfn1p  19578  lspextmo  19828  2idlval  20006  aspsubrg  20105  psrbagsn  20275  pjfval  20850  pjpm  20852  ofco2  21060  basdif0  21561  tgval2  21564  eltg3  21570  tgcl  21577  tgdom  21586  tgidm  21588  ppttop  21615  epttop  21617  ntropn  21657  ntrin  21669  mretopd  21700  neiptoptop  21739  restfpw  21787  neitr  21788  restcls  21789  cncls  21882  cnpresti  21896  cnprest  21897  cmpsublem  22007  cmpsub  22008  fiuncmp  22012  indisconn  22026  connsub  22029  iunconnlem  22035  islly2  22092  cldllycmp  22103  kgentopon  22146  ptbasfi  22189  ptcnplem  22229  txcnmpt  22232  txcmplem2  22250  hausdiag  22253  txkgen  22260  xkococnlem  22267  qtoptop2  22307  basqtop  22319  fbssfi  22445  filin  22462  infil  22471  fbasrn  22492  fgtr  22498  ufprim  22517  flimrest  22591  txflf  22614  fclsrest  22632  alexsubALTlem4  22658  tsmsres  22752  tsmsxplem1  22761  ustund  22830  trust  22838  utoptop  22843  restutop  22846  cfiluweak  22904  xmetres  22974  metres  22975  blin2  23039  setsmstopn  23088  metrest  23134  ressxms  23135  tgioo  23404  xrsmopn  23420  reconnlem1  23434  xrge0tsms  23442  tcphcph  23840  cfilresi  23898  cfilres  23899  caussi  23900  causs  23901  relcmpcmet  23921  minveclem4a  24033  ismbl2  24128  cmmbl  24135  nulmbl2  24137  unmbl  24138  shftmbl  24139  volinun  24147  voliunlem1  24151  voliunlem2  24152  ioombl1lem4  24162  ioombl1  24163  uniioombllem2  24184  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombl  24190  volivth  24208  vitalilem3  24211  vitalilem4  24212  vitalilem5  24213  vitali  24214  mbfadd  24262  mbfsub  24263  i1fadd  24296  itg1addlem2  24298  itg1addlem4  24300  itg1addlem5  24301  itg1climres  24315  mbfmul  24327  itg2splitlem  24349  itg2split  24350  limcresi  24483  limciun  24492  dvreslem  24507  dvres2lem  24508  dvres  24509  dvres3a  24512  dvaddbr  24535  dvmulbr  24536  dvfsumle  24618  dvfsumabs  24620  ig1peu  24765  pilem2  25040  pilem3  25041  rlimcnp2  25544  ppisval  25681  ppifi  25683  ppiprm  25728  chtprm  25730  chtdif  25735  efchtdvds  25736  ppidif  25740  ppiltx  25754  prmorcht  25755  ppiub  25780  chtlepsi  25782  pclogsum  25791  vmasum  25792  chpval2  25794  chpub  25796  2sqlem8  26002  chebbnd1lem1  26045  chtppilimlem1  26049  rpvmasum2  26088  dchrisum0re  26089  rplogsum  26103  dirith2  26104  axtgcgrrflx  26248  axtgcgrid  26249  axtgsegcon  26250  axtg5seg  26251  axtgbtwnid  26252  axtgpasch  26253  axtgcont1  26254  phnv  28591  minvecolem2  28652  minvecolem3  28653  minvecolem5  28658  minvecolem6  28659  minvecolem7  28660  hlimcaui  29013  chdmm1i  29254  chabs1  29293  chabs2  29294  ledii  29313  lejdii  29315  pjoml4i  29364  cmbr3i  29377  cmbr4i  29378  cmm1i  29383  osumcor2i  29421  3oalem4  29442  pjssmii  29458  pjocini  29475  pjini  29476  mayete3i  29505  riesz4  29841  riesz1  29842  cnlnadjeui  29854  cnlnadjeu  29855  cnlnssadj  29857  nmopadjlei  29865  pjin1i  29969  pjclem1  29972  stji1i  30019  stm1i  30020  dmdbr2  30080  ssmd1  30088  mdslj2i  30097  mdsl2bi  30100  mdslmd1lem1  30102  mdslmd2i  30107  atomli  30159  atcvat4i  30174  sumdmdlem2  30196  dmdbr5ati  30199  dmdbr6ati  30200  dmdbr7ati  30201  disjxpin  30338  imadifxp  30351  nfpconfp  30377  off2  30388  ffsrn  30465  gsummptres  30690  xrge0tsmsd  30692  ordtrestNEW  31164  qqhnm  31231  qqhcn  31232  rrhre  31262  indsumin  31281  indf1ofs  31285  esumval  31305  esumel  31306  gsumesum  31318  esumlub  31319  esumcst  31322  esumfsup  31329  esumpcvgval  31337  esumcvg  31345  sigainb  31395  ldgenpisyslem1  31422  measinb2  31482  sibfinima  31597  sibfof  31598  eulerpartlemelr  31615  eulerpartlem1  31625  eulerpartgbij  31630  eulerpartlemgu  31635  eulerpartlemgs2  31638  sseqf  31650  ballotlemfelz  31748  ballotlemfp1  31749  reprinrn  31889  reprinfz1  31893  hgt750lemd  31919  bnj1292  32087  connpconn  32482  iccllysconn  32497  cvmsss2  32521  cvmcov2  32522  cvmopnlem  32525  cvmliftmolem2  32529  cvmliftlem15  32545  cvmlift2lem12  32561  mvrsfpw  32753  msrf  32789  elmsta  32795  mthmpps  32829  nepss  32948  dfon2lem4  33031  frrlem4  33126  frrlem13  33135  frrlem15  33142  nosupbnd1lem1  33208  nosupbnd2  33216  txpss3v  33339  fixssdm  33367  fixssrn  33368  limitssson  33372  fneer  33701  neibastop1  33707  neibastop2lem  33708  filnetlem3  33728  ontopbas  33776  bj-disj2r  34343  bj-restpw  34386  bj-discrmoore  34406  bj-idres  34455  bj-fvsnun2  34541  bj-ablssgrp  34561  bj-flddrng  34573  taupilemrplb  34604  taupilem2  34606  taupi  34607  ptrest  34906  poimirlem29  34936  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  mbfposadd  34954  sstotbnd2  35067  ssbnd  35081  heibor1lem  35102  heiborlem1  35104  heiborlem3  35106  heiborlem5  35108  heiborlem6  35109  heiborlem10  35113  heibor  35114  opidonOLD  35145  exidcl  35169  flddivrng  35292  iss2  35616  xrnss3v  35639  refrelsredund2  35883  lshpinN  36140  lcvexchlem5  36189  pmodlem2  36998  pmod1i  36999  pmodN  37001  osumcllem7N  37113  pexmidlem4N  37124  pl42lem3N  37132  djaclN  38287  dihoml4c  38527  dochdmj1  38541  djhcl  38551  dochexmidlem4  38614  mapd1o  38799  mapdin  38813  elrfi  39311  elrfirn  39312  elrfirn2  39313  ismrcd1  39315  istopclsd  39317  isnacs2  39323  mrefg3  39325  isnacs3  39327  diophrw  39376  diophin  39389  aomclem2  39675  islmodfg  39689  lsmfgcl  39694  lmhmfgima  39704  lmhmfgsplit  39706  lmhmlnmsplit  39707  pwfi2f1o  39716  hbt  39750  harval3  39924  elinintrab  39957  trrelind  40030  rp-imass  40137  clsk3nimkb  40410  isotone2  40419  onfrALTlem2  40900  onfrALTlem2VD  41243  unirestss  41410  inmap  41492  fsumiunss  41876  islptre  41920  sumnnodd  41931  limclner  41952  liminfval4  42090  liminfval3  42091  cnrefiisplem  42130  cncfuni  42189  ismbl3  42291  ismbl4  42298  fouriersw  42536  qndenserrnbllem  42599  salincl  42628  salgencntex  42646  sge0less  42694  sge0resplit  42708  sge0split  42711  sge0iunmptlemre  42717  carageniuncllem1  42823  carageniuncllem2  42824  caragenel2d  42834  hspmbllem3  42930  hspmbl  42931  ovolval2lem  42945  sssmf  43035  smfaddlem1  43059  smflimlem2  43068  smflimlem3  43069  smflimlem4  43070  smfres  43085  smfmullem4  43089  smfsuplem1  43105  rngcbas  44256  rngchomfval  44257  rngccofval  44261  dfrngc2  44263  rnghmsscmap2  44264  rnghmsscmap  44265  rngcsect  44271  funcrngcsetc  44289  ringcbas  44302  ringchomfval  44303  ringccofval  44307  dfringc2  44309  rhmsscmap2  44310  rhmsscmap  44311  rhmsscrnghm  44317  ringcsect  44322  funcringcsetc  44326  funcringcsetcALTV2lem9  44335  fldc  44374  fldhmsubc  44375  rngcrescrhm  44376  rhmsubclem1  44377  fldcALTV  44392  fldhmsubcALTV  44393  rngcrescrhmALTV  44394  rhmsubcALTVlem1  44395  setrec2fun  44815  setrec2lem1  44816