Theorem inss1 4188

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

Syntax hints:   ∩ cin 3902   ⊆ wss 3903

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 3438  df-in 3910  df-ss 3920

This theorem is referenced by:  inss2  4189  ssinss1  4197  unabs  4216  nssinpss  4218  dfin4  4229  inv1  4349  disjdif  4423  ifssun  4494  uniintsn  4935  wefrc  5613  relin1  5755  resss  5952  resmpt3  5989  cnvcnvss  6143  resdmss  6184  resssxp  6218  predss  6257  ordtri3or  6339  onfr  6346  ordelinel  6410  funin  6558  funimass2  6565  fnresin1  6607  fnres  6609  fresin  6693  fresaun  6695  nfvres  6861  ssimaex  6908  fneqeql2  6981  fnfvimad  7170  funiunfv  7184  isoini2  7276  ofrfvalg  7621  ofval  7624  ofrval  7625  off  7631  ofres  7632  ofco  7638  fparlem3  8047  fparlem4  8048  frrlem4  8222  frrlem13  8231  smores  8275  smores2  8277  tfrlem5  8302  pmresg  8797  sbthlem7  9010  sbthcl  9016  infi  9159  imafi  9204  ixpfi2  9240  unifpw  9245  elfiun  9320  dffi3  9321  marypha1lem  9323  ordtypelem6  9415  ordtypelem7  9416  ordtypelem8  9417  wdomima2g  9478  frmin  9645  frrlem15  9653  frrlem16  9654  tskwe  9846  ackbij1lem15  10127  ackbij1lem16  10128  fin23lem23  10220  fin23lem22  10221  fin23lem19  10230  brdom3  10422  brdom5  10423  brdom4  10424  imadomg  10428  fpwwe2lem11  10535  canthp1lem2  10547  wunin  10607  tskin  10653  gruima  10696  ingru  10709  gruina  10712  grur1a  10713  nqerf  10824  nqerrel  10826  hashun3  14291  hashin  14318  hashdif  14320  xptrrel  14887  rexanuz  15253  limsupgle  15384  rlimres  15465  lo1res  15466  lo1resb  15471  rlimresb  15472  o1resb  15473  lo1eq  15475  rlimeq  15476  o1of2  15520  o1rlimmul  15526  isercolllem2  15573  isercolllem3  15574  isercoll  15575  incexclem  15743  incexc  15744  bitsinvp1  16360  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadaddlem  16377  sadasslem  16381  sadeq  16383  bitsres  16384  smuval2  16393  smupval  16399  smueqlem  16401  smumul  16404  ramub2  16926  ramub1lem2  16939  fvsetsid  17079  ressbasss2  17152  ressinbas  17156  ressress  17158  submre  17507  isacs1i  17563  mreacs  17564  acsfn  17565  invss  17668  sscres  17730  catcisolem  18017  catciso  18018  isacs5lem  18451  psss  18486  tsrss  18495  tsrdir  18510  sylow2a  19498  lsmmod  19554  gsumzres  19788  gsumzaddlem  19800  dprddisj2  19920  ablfac1eu  19954  isunit  20258  rngcbas  20506  rngchomfval  20507  rngccofval  20511  dfrngc2  20513  rnghmsscmap2  20514  rnghmsscmap  20515  rngcsect  20521  funcrngcsetc  20525  ringcbas  20535  ringchomfval  20536  ringccofval  20540  dfringc2  20542  rhmsscmap2  20543  rhmsscmap  20544  rhmsscrnghm  20550  ringcsect  20555  funcringcsetc  20559  rngcrescrhm  20569  rhmsubclem1  20570  fldc  20669  fldhmsubc  20670  acsfn1p  20684  lspextmo  20960  2idlval  21158  pjfval  21613  pjpm  21615  aspsubrg  21783  psrbagsn  21968  ofco2  22336  basdif0  22838  tgval2  22841  eltg3  22847  tgcl  22854  tgdom  22863  tgidm  22865  ppttop  22892  epttop  22894  ntropn  22934  ntrin  22946  mretopd  22977  neiptoptop  23016  restfpw  23064  neitr  23065  restcls  23066  cncls  23159  cnpresti  23173  cnprest  23174  cmpsublem  23284  cmpsub  23285  fiuncmp  23289  indisconn  23303  connsub  23306  iunconnlem  23312  islly2  23369  cldllycmp  23380  kgentopon  23423  ptbasfi  23466  ptcnplem  23506  txcnmpt  23509  txcmplem2  23527  hausdiag  23530  txkgen  23537  xkococnlem  23544  qtoptop2  23584  basqtop  23596  fbssfi  23722  filin  23739  infil  23748  fbasrn  23769  fgtr  23775  ufprim  23794  flimrest  23868  txflf  23891  fclsrest  23909  alexsubALTlem4  23935  tsmsres  24029  tsmsxplem1  24038  ustund  24107  trust  24115  utoptop  24120  restutop  24123  cfiluweak  24180  xmetres  24250  metres  24251  blin2  24315  setsmstopn  24364  metrest  24410  ressxms  24411  tgioo  24682  xrsmopn  24699  reconnlem1  24713  xrge0tsms  24721  tcphcph  25135  cfilresi  25193  cfilres  25194  caussi  25195  causs  25196  relcmpcmet  25216  minveclem4a  25328  ismbl2  25426  cmmbl  25433  nulmbl2  25435  unmbl  25436  shftmbl  25437  volinun  25445  voliunlem1  25449  voliunlem2  25450  ioombl1lem4  25460  ioombl1  25461  uniioombllem2  25482  uniioombllem3  25484  uniioombllem4  25485  uniioombllem5  25486  uniioombl  25488  volivth  25506  vitalilem3  25509  vitalilem4  25510  vitalilem5  25511  vitali  25512  mbfadd  25560  mbfsub  25561  i1fadd  25594  itg1addlem2  25596  itg1addlem4  25598  itg1addlem5  25599  itg1climres  25613  mbfmul  25625  itg2splitlem  25647  itg2split  25648  limcresi  25784  limciun  25793  dvreslem  25808  dvres2lem  25809  dvres  25810  dvres3a  25813  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  ig1peu  26078  pilem2  26360  pilem3  26361  rlimcnp2  26874  ppisval  27012  ppifi  27014  ppiprm  27059  chtprm  27061  chtdif  27066  efchtdvds  27067  ppidif  27071  ppiltx  27085  prmorcht  27086  ppiub  27113  chtlepsi  27115  pclogsum  27124  vmasum  27125  chpval2  27127  chpub  27129  2sqlem8  27335  chebbnd1lem1  27378  chtppilimlem1  27382  rpvmasum2  27421  dchrisum0re  27422  rplogsum  27436  dirith2  27437  nosupbnd1lem1  27618  nosupbnd2  27626  noinfbnd1lem1  27633  axtgcgrrflx  28407  axtgcgrid  28408  axtgsegcon  28409  axtg5seg  28410  axtgbtwnid  28411  axtgpasch  28412  axtgcont1  28413  phnv  30758  minvecolem2  30819  minvecolem3  30820  minvecolem5  30825  minvecolem6  30826  minvecolem7  30827  hlimcaui  31180  chdmm1i  31421  chabs1  31460  chabs2  31461  ledii  31480  lejdii  31482  pjoml4i  31531  cmbr3i  31544  cmbr4i  31545  cmm1i  31550  osumcor2i  31588  3oalem4  31609  pjssmii  31625  pjocini  31642  pjini  31643  mayete3i  31672  riesz4  32008  riesz1  32009  cnlnadjeui  32021  cnlnadjeu  32022  cnlnssadj  32024  nmopadjlei  32032  pjin1i  32136  pjclem1  32139  stji1i  32186  stm1i  32187  dmdbr2  32247  ssmd1  32255  mdslj2i  32264  mdsl2bi  32267  mdslmd1lem1  32269  mdslmd2i  32274  atomli  32326  atcvat4i  32341  sumdmdlem2  32363  dmdbr5ati  32366  dmdbr6ati  32367  dmdbr7ati  32368  indifbi  32464  disjxpin  32532  imadifxp  32545  nfpconfp  32575  off2  32584  ffsrn  32672  indsumin  32805  indf1ofs  32809  gsummptres  33005  xrge0tsmsd  33015  idlinsubrg  33368  ordtrestNEW  33888  qqhnm  33957  qqhcn  33958  rrhre  33988  esumval  34013  esumel  34014  gsumesum  34026  esumlub  34027  esumcst  34030  esumfsup  34037  esumpcvgval  34045  esumcvg  34053  sigainb  34103  ldgenpisyslem1  34130  measinb2  34190  sibfinima  34307  sibfof  34308  eulerpartlemelr  34325  eulerpartlem1  34335  eulerpartgbij  34340  eulerpartlemgu  34345  eulerpartlemgs2  34348  sseqf  34360  ballotlemfelz  34459  ballotlemfp1  34460  reprinrn  34586  reprinfz1  34590  hgt750lemd  34616  bnj1292  34782  connpconn  35212  iccllysconn  35227  cvmsss2  35251  cvmcov2  35252  cvmopnlem  35255  cvmliftmolem2  35259  cvmliftlem15  35275  cvmlift2lem12  35291  mvrsfpw  35483  msrf  35519  elmsta  35525  mthmpps  35559  nepss  35695  dfon2lem4  35764  txpss3v  35856  fixssdm  35884  fixssrn  35885  limitssson  35889  fneer  36331  neibastop1  36337  neibastop2lem  36338  filnetlem3  36358  ontopbas  36406  bj-disj2r  37006  bj-restpw  37070  bj-discrmoore  37089  bj-idres  37138  bj-fvsnun2  37234  bj-ablssgrp  37254  bj-fldssdrng  37266  taupilemrplb  37298  taupilem2  37300  taupi  37301  ptrest  37603  poimirlem29  37633  mblfinlem3  37643  mblfinlem4  37644  ismblfin  37645  mbfposadd  37651  sstotbnd2  37758  ssbnd  37772  heibor1lem  37793  heiborlem1  37795  heiborlem3  37797  heiborlem5  37799  heiborlem6  37800  heiborlem10  37804  heibor  37805  opidonOLD  37836  exidcl  37860  flddivrng  37983  iss2  38316  xrnss3v  38344  refrelsredund2  38614  lshpinN  38972  lcvexchlem5  39021  pmodlem2  39830  pmod1i  39831  pmodN  39833  osumcllem7N  39945  pexmidlem4N  39956  pl42lem3N  39964  djaclN  41119  dihoml4c  41359  dochdmj1  41373  djhcl  41383  dochexmidlem4  41446  mapd1o  41631  mapdin  41645  unitscyglem5  42176  redvmptabs  42337  elrfi  42671  elrfirn  42672  elrfirn2  42673  ismrcd1  42675  istopclsd  42677  isnacs2  42683  mrefg3  42685  isnacs3  42687  diophrw  42736  diophin  42749  aomclem2  43032  islmodfg  43046  lsmfgcl  43051  lmhmfgima  43061  lmhmfgsplit  43063  lmhmlnmsplit  43064  pwfi2f1o  43073  hbt  43107  ofoafg  43331  harval3  43515  elinintrab  43554  trrelind  43642  clsk3nimkb  44017  isotone2  44026  ismnushort  44278  onfrALTlem2  44524  onfrALTlem2VD  44866  wfac8prim  44980  unirestss  45106  inmap  45191  fsumiunss  45560  islptre  45604  sumnnodd  45615  limclner  45636  liminfval4  45774  liminfval3  45775  cnrefiisplem  45814  cncfuni  45871  ismbl3  45971  ismbl4  45978  fouriersw  46216  qndenserrnbllem  46279  salincl  46309  salgencntex  46328  sge0less  46377  sge0resplit  46391  sge0split  46394  sge0iunmptlemre  46400  carageniuncllem1  46506  carageniuncllem2  46507  caragenel2d  46517  hspmbllem3  46613  hspmbl  46614  ovolval2lem  46628  sssmf  46723  smfaddlem1  46748  smflimlem2  46757  smflimlem3  46758  smflimlem4  46759  smfres  46775  smfmullem4  46779  smfsuplem1  46796  fcoreslem2  47052  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