Theorem inss1 4135

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

This proof depends on syntax axioms:   ⊆ wss 3899   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-in 4093

This theorem is used by:  inss2  4136  ssinss1  4144  ssinss1OLD  4145  unabs  4212  nssinpss  4214  dfin4  4225  inv1  4350  vvin  4361  ifssun  4502  uniin  4893  uniintsn  4947  wefrc  5648  relin1  5794  resss  5996  resindm  6024  resmpt3  6035  rnin  6142  cnvcnvssOLD  6192  resdmss  6242  resssxp  6278  predss  6318  ordtri3or  6401  onfr  6408  ordelinel  6472  funin  6624  funimass2  6631  fnresin1  6672  fnres  6674  fresin  6759  fresaun  6761  nfvres  6931  ssimaex  6978  fneqeql2  7054  fnfvimad  7247  funiunfv  7259  isoini2  7354  ofrfvalg  7708  ofval  7711  ofrval  7712  off  7718  ofres  7719  ofco  7725  fparlem3  8135  fparlem4  8136  frrlem4  8318  frrlem13  8327  smores2  8373  tfrlem5  8398  pmresg  8909  sbthlem7  9123  sbthcl  9129  infi  9272  imafi  9318  ixpfi2  9350  unifpw  9355  elfiun  9432  dffi3  9433  marypha1lem  9435  ordtypelem6  9527  ordtypelem7  9528  ordtypelem8  9529  wdomima2g  9590  frmin  9763  frrlem15  9771  frrlem16  9772  setrec2fun  9983  tskwe  10041  ackbij1lem15  10321  ackbij1lem16  10322  fin23lem23  10414  fin23lem22  10415  fin23lem19  10424  brdom3  10617  brdom5  10618  brdom4  10619  imadomg  10623  imadomnum  10624  fpwwe2lem11  10736  canthp1lem2  10748  wunin  10808  tskin  10854  gruima  10897  ingru  10910  gruina  10913  grur1a  10914  nqerf  11025  nqerrel  11027  hashun3  14538  hashin  14566  hashdif  14568  xptrrel  15145  rexanuz  15525  limsupgle  15656  rlimres  15737  lo1res  15738  lo1resb  15743  rlimresb  15744  o1resb  15745  lo1eq  15747  rlimeq  15748  o1of2  15792  o1rlimmul  15798  isercolllem2  15845  isercolllem3  15846  isercoll  15847  incexclem  16017  incexc  16018  bitsinvp1  16631  sadcaddlem  16639  sadadd2lem  16641  sadadd3  16643  sadaddlem  16648  sadasslem  16652  sadeq  16654  bitsres  16655  smuval2  16664  smupval  16670  smueqlem  16672  smumul  16675  ramub2  17204  ramub1lem2  17217  fvsetsid  17358  ressbasss2  17431  ressinbas  17435  ressress  17437  submre  17787  isacs1i  17843  mreacs  17844  acsfn  17845  invss  17948  sscres  18010  catcisolem  18297  catciso  18298  isacs5lem  18731  psss  18766  tsrss  18775  tsrdir  18790  sylow2a  19845  lsmmod  19901  gsumzres  20135  gsumzaddlem  20147  dprddisj2  20267  ablfac1eu  20301  isunit  20615  rngcbas  20885  rngchomfval  20886  rngccofval  20890  dfrngc2  20892  rnghmsscmap2  20893  rnghmsscmap  20894  rngcsect  20900  funcrngcsetc  20904  ringcbas  20914  ringchomfval  20915  ringccofval  20919  dfringc2  20921  rhmsscmap2  20922  rhmsscmap  20923  rhmsscrnghm  20929  ringcsect  20934  funcringcsetc  20938  rngcrescrhm  20948  rhmsubclem1  20949  fldc  21053  fldhmsubc  21054  acsfn1p  21068  lspextmo  21343  2idlval  21556  pjfval  22024  pjpm  22026  aspsubrg  22195  psrbagsn  22384  ofco2  22778  basdif0  23283  tgval2  23286  eltg3  23292  tgcl  23299  tgdom  23308  tgidm  23310  ppttop  23337  epttop  23339  ntropn  23379  ntrin  23391  mretopd  23422  neiptoptop  23461  restfpw  23509  neitr  23510  restcls  23511  cncls  23604  cnpresti  23618  cnprest  23619  cmpsublem  23729  cmpsub  23730  fiuncmp  23734  indisconn  23748  connsub  23751  iunconnlem  23757  islly2  23815  cldllycmp  23826  kgentopon  23869  ptbasfi  23912  ptcnplem  23952  txcnmpt  23955  txcmplem2  23973  hausdiag  23976  txkgen  23983  xkococnlem  23990  qtoptop2  24030  basqtop  24042  fbssfi  24168  filin  24185  infil  24194  fbasrn  24215  fgtr  24221  ufprim  24240  flimrest  24314  txflf  24337  fclsrest  24355  alexsubALTlem4  24381  tsmsres  24475  tsmsxplem1  24484  ustund  24553  trust  24560  utoptop  24565  restutop  24568  cfiluweak  24625  xmetres  24695  metres  24696  blin2  24760  setsmstopn  24809  metrest  24855  ressxms  24856  tgioo  25127  xrsmopn  25144  reconnlem1  25158  xrge0tsms  25166  tcphcph  25570  cfilresi  25628  cfilres  25629  caussi  25630  causs  25631  relcmpcmet  25651  minveclem4a  25763  ismbl2  25860  cmmbl  25867  nulmbl2  25869  unmbl  25870  shftmbl  25871  volinun  25879  voliunlem1  25883  voliunlem2  25884  ioombl1lem4  25894  ioombl1  25895  uniioombllem2  25916  uniioombllem3  25918  uniioombllem4  25919  uniioombllem5  25920  uniioombl  25922  volivth  25940  vitalilem3  25943  vitalilem4  25944  vitalilem5  25945  vitali  25946  mbfadd  25994  mbfsub  25995  i1fadd  26028  itg1addlem2  26030  itg1addlem4  26032  itg1addlem5  26033  itg1climres  26047  mbfmul  26059  itg2splitlem  26081  itg2split  26082  limcresi  26217  limciun  26226  dvreslem  26241  dvres2lem  26242  dvres  26243  dvres3a  26246  dvaddbr  26270  dvmulbr  26271  dvfsumle  26353  dvfsumabs  26355  ig1peu  26505  pilem2  26791  pilem3  26792  rlimcnp2  27306  ppisval  27443  ppifi  27445  ppiprm  27490  chtprm  27492  chtdif  27497  efchtdvds  27498  ppidif  27502  ppiltx  27516  prmorcht  27517  ppiub  27543  chtlepsi  27545  pclogsum  27554  vmasum  27555  chpval2  27557  chpub  27559  2sqlem8  27765  chebbnd1lem1  27808  chtppilimlem1  27812  rpvmasum2  27851  dchrisum0re  27852  rplogsum  27866  dirith2  27867  nosupbnd1lem1  28077  nosupbnd2  28085  noinfbnd1lem1  28092  axtgcgrrflx  28936  axtgcgrid  28937  axtgsegcon  28938  axtg5seg  28939  axtgbtwnid  28940  axtgpasch  28941  axtgcont1  28942  phnv  31428  minvecolem2  31489  minvecolem3  31490  minvecolem5  31495  minvecolem6  31496  minvecolem7  31497  hlimcaui  31850  chdmm1i  32091  chabs1  32130  chabs2  32131  ledii  32150  lejdii  32152  pjoml4i  32201  cmbr3i  32214  cmbr4i  32215  cmm1i  32220  osumcor2i  32258  3oalem4  32279  pjssmii  32295  pjocini  32312  pjini  32313  mayete3i  32342  riesz4  32678  riesz1  32679  cnlnadjeui  32691  cnlnadjeu  32692  cnlnssadj  32694  nmopadjlei  32702  pjin1i  32806  pjclem1  32809  stji1i  32856  stm1i  32857  dmdbr2  32917  ssmd1  32925  mdslj2i  32934  mdsl2bi  32937  mdslmd1lem1  32939  mdslmd2i  32944  atomli  32996  atcvat4i  33011  sumdmdlem2  33033  dmdbr5ati  33036  dmdbr6ati  33037  dmdbr7ati  33038  indifbi  33170  disjxpin  33236  imadifxp  33249  nfpconfp  33280  off2  33289  ffsrn  33373  indsumin  33481  indf1ofs  33486  gsummptres  33666  xrge0tsmsd  33687  idlinsubrg  34034  ordtrestNEW  34606  qqhnm  34675  qqhcn  34676  rrhre  34706  esumval  34731  esumel  34732  gsumesum  34744  esumlub  34745  esumcst  34748  esumfsup  34755  esumpcvgval  34763  esumcvg  34771  sigainb  34822  ldgenpisyslem1  34849  measinb2  34909  sibfinima  35024  sibfof  35025  eulerpartlemelr  35042  eulerpartlem1  35052  eulerpartgbij  35057  eulerpartlemgu  35062  eulerpartlemgs2  35065  sseqf  35077  ballotlemfelz  35176  ballotlemfp1  35177  reprinrn  35300  reprinfz1  35304  hgt750lemd  35330  bnj1292  35498  connpconn  36121  iccllysconn  36136  cvmsss2  36160  cvmcov2  36161  cvmopnlem  36164  cvmliftmolem2  36168  cvmliftlem15  36184  cvmlift2lem12  36200  mvrsfpw  36392  msrf  36428  elmsta  36434  mthmpps  36468  nepss  36610  dfon2lem4  36675  txpss3v  36767  fixssdm  36795  fixssrn  36796  limitssson  36800  fneer  37268  neibastop1  37274  neibastop2lem  37275  filnetlem3  37295  ontopbas  37343  bj-disj2r  38068  bj-restpw  38152  bj-discrmoore  38171  bj-idres  38221  bj-fvsnun2  38317  bj-ablssgrp  38337  bj-fldssdrng  38349  taupilemrplb  38381  taupilem2  38383  taupi  38384  ptrest  38677  poimirlem29  38707  mblfinlem3  38717  mblfinlem4  38718  ismblfin  38719  mbfposadd  38725  sstotbnd2  38848  ssbnd  38862  heibor1lem  38883  heiborlem1  38885  heiborlem3  38887  heiborlem5  38889  heiborlem6  38890  heiborlem10  38894  heibor  38895  opidonOLD  38926  exidcl  38950  flddivrng  39073  iss2  39416  xrnss3v  39453  refrelsredund2  39789  lshpinN  40186  lcvexchlem5  40235  pmodlem2  41044  pmod1i  41045  pmodN  41047  osumcllem7N  41159  pexmidlem4N  41170  pl42lem3N  41178  djaclN  42333  dihoml4c  42573  dochdmj1  42587  djhcl  42597  dochexmidlem4  42660  mapd1o  42845  mapdin  42859  unitscyglem5  43389  redvmptabs  43551  elrfi  43845  elrfirn  43846  elrfirn2  43847  ismrcd1  43849  istopclsd  43851  isnacs2  43857  mrefg3  43859  isnacs3  43861  diophrw  43910  diophin  43923  aomclem2  44197  islmodfg  44211  lsmfgcl  44216  lmhmfgima  44226  lmhmfgsplit  44228  lmhmlnmsplit  44229  pwfi2f1o  44238  hbt  44272  ofoafg  44496  harval3  44679  elinintrab  44718  trrelind  44805  clsk3nimkb  45180  isotone2  45189  ismnushort  45425  onfrALTlem2  45668  onfrALTlem2VD  46010  wfac8prim  46131  unirestss  46278  inmap  46361  fsumiunss  46726  islptre  46770  sumnnodd  46781  limclner  46800  liminfval4  46938  liminfval3  46939  cnrefiisplem  46978  cncfuni  47035  ismbl3  47135  ismbl4  47142  fouriersw  47380  qndenserrnbllem  47443  salincl  47473  salgencntex  47492  sge0less  47541  sge0resplit  47555  sge0split  47558  sge0iunmptlemre  47564  carageniuncllem1  47670  carageniuncllem2  47671  caragenel2d  47681  hspmbllem3  47777  hspmbl  47778  ovolval2lem  47792  sssmf  47887  smfaddlem1  47912  smflimlem2  47921  smflimlem3  47922  smflimlem4  47923  smfres  47939  smfmullem4  47943  smfsuplem1  47960  wrddrin  48036  chndrin  48041  chnrrin  48046  fcoreslem2  48273  indprmfz  48854  ppivalnn  48856  rngcrescrhmALTV  49516  rhmsubcALTVlem1  49517  funcringcsetcALTV2lem9  49534  fldcALTV  49568  fldhmsubcALTV  49569  iscnrm3llem2  50203  uptrlem1  50465  uptrlem2  50466  uptrlem3  50467  uptra  50470  uptrar  50471  uobeqw  50474  uptr2  50476  uptr2a  50477  fucoppcfunc  50686