Theorem inss1 4182

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ss 3916

This theorem is used by:  inss2  4183  ssinss1  4191  ssinss1OLD  4192  unabs  4211  nssinpss  4213  dfin4  4224  inv1  4348  vvin  4359  ifssun  4500  uniin  4891  uniintsn  4945  wefrc  5649  relin1  5793  resss  5994  resindm  6023  resmpt3  6034  rnin  6137  cnvcnvssOLD  6188  resdmss  6231  resssxp  6267  predss  6307  ordtri3or  6390  onfr  6397  ordelinel  6461  funin  6610  funimass2  6617  fnresin1  6658  fnres  6660  fresin  6745  fresaun  6747  nfvres  6917  ssimaex  6964  fneqeql2  7040  fnfvimad  7234  funiunfv  7246  isoini2  7341  ofrfvalg  7687  ofval  7690  ofrval  7691  off  7697  ofres  7698  ofco  7704  fparlem3  8112  fparlem4  8113  frrlem4  8289  frrlem13  8298  smores  8342  smores2  8344  tfrlem5  8369  pmresg  8880  sbthlem7  9094  sbthcl  9100  infi  9243  imafi  9288  ixpfi2  9320  unifpw  9325  elfiun  9403  dffi3  9404  marypha1lem  9406  ordtypelem6  9498  ordtypelem7  9499  ordtypelem8  9500  wdomima2g  9561  frmin  9734  frrlem15  9742  frrlem16  9743  tskwe  9958  ackbij1lem15  10238  ackbij1lem16  10239  fin23lem23  10331  fin23lem22  10332  fin23lem19  10341  brdom3  10534  brdom5  10535  brdom4  10536  imadomg  10540  imadomnum  10541  fpwwe2lem11  10653  canthp1lem2  10665  wunin  10725  tskin  10771  gruima  10814  ingru  10827  gruina  10830  grur1a  10831  nqerf  10942  nqerrel  10944  hashun3  14451  hashin  14479  hashdif  14481  xptrrel  15056  rexanuz  15436  limsupgle  15567  rlimres  15648  lo1res  15649  lo1resb  15654  rlimresb  15655  o1resb  15656  lo1eq  15658  rlimeq  15659  o1of2  15703  o1rlimmul  15709  isercolllem2  15756  isercolllem3  15757  isercoll  15758  incexclem  15928  incexc  15929  bitsinvp1  16542  sadcaddlem  16550  sadadd2lem  16552  sadadd3  16554  sadaddlem  16559  sadasslem  16563  sadeq  16565  bitsres  16566  smuval2  16575  smupval  16581  smueqlem  16583  smumul  16586  ramub2  17109  ramub1lem2  17122  fvsetsid  17263  ressbasss2  17336  ressinbas  17340  ressress  17342  submre  17692  isacs1i  17748  mreacs  17749  acsfn  17750  invss  17853  sscres  17915  catcisolem  18202  catciso  18203  isacs5lem  18636  psss  18671  tsrss  18680  tsrdir  18695  sylow2a  19749  lsmmod  19805  gsumzres  20039  gsumzaddlem  20051  dprddisj2  20171  ablfac1eu  20205  isunit  20517  rngcbas  20786  rngchomfval  20787  rngccofval  20791  dfrngc2  20793  rnghmsscmap2  20794  rnghmsscmap  20795  rngcsect  20801  funcrngcsetc  20805  ringcbas  20815  ringchomfval  20816  ringccofval  20820  dfringc2  20822  rhmsscmap2  20823  rhmsscmap  20824  rhmsscrnghm  20830  ringcsect  20835  funcringcsetc  20839  rngcrescrhm  20849  rhmsubclem1  20850  fldc  20953  fldhmsubc  20954  acsfn1p  20968  lspextmo  21243  2idlval  21456  pjfval  21922  pjpm  21924  aspsubrg  22093  psrbagsn  22282  ofco2  22676  basdif0  23181  tgval2  23184  eltg3  23190  tgcl  23197  tgdom  23206  tgidm  23208  ppttop  23235  epttop  23237  ntropn  23277  ntrin  23289  mretopd  23320  neiptoptop  23359  restfpw  23407  neitr  23408  restcls  23409  cncls  23502  cnpresti  23516  cnprest  23517  cmpsublem  23627  cmpsub  23628  fiuncmp  23632  indisconn  23646  connsub  23649  iunconnlem  23655  islly2  23713  cldllycmp  23724  kgentopon  23767  ptbasfi  23810  ptcnplem  23850  txcnmpt  23853  txcmplem2  23871  hausdiag  23874  txkgen  23881  xkococnlem  23888  qtoptop2  23928  basqtop  23940  fbssfi  24066  filin  24083  infil  24092  fbasrn  24113  fgtr  24119  ufprim  24138  flimrest  24212  txflf  24235  fclsrest  24253  alexsubALTlem4  24279  tsmsres  24373  tsmsxplem1  24382  ustund  24451  trust  24458  utoptop  24463  restutop  24466  cfiluweak  24523  xmetres  24593  metres  24594  blin2  24658  setsmstopn  24707  metrest  24753  ressxms  24754  tgioo  25025  xrsmopn  25042  reconnlem1  25056  xrge0tsms  25064  tcphcph  25468  cfilresi  25526  cfilres  25527  caussi  25528  causs  25529  relcmpcmet  25549  minveclem4a  25661  ismbl2  25758  cmmbl  25765  nulmbl2  25767  unmbl  25768  shftmbl  25769  volinun  25777  voliunlem1  25781  voliunlem2  25782  ioombl1lem4  25792  ioombl1  25793  uniioombllem2  25814  uniioombllem3  25816  uniioombllem4  25817  uniioombllem5  25818  uniioombl  25820  volivth  25838  vitalilem3  25841  vitalilem4  25842  vitalilem5  25843  vitali  25844  mbfadd  25892  mbfsub  25893  i1fadd  25926  itg1addlem2  25928  itg1addlem4  25930  itg1addlem5  25931  itg1climres  25945  mbfmul  25957  itg2splitlem  25979  itg2split  25980  limcresi  26115  limciun  26124  dvreslem  26139  dvres2lem  26140  dvres  26141  dvres3a  26144  dvaddbr  26168  dvmulbr  26169  dvfsumle  26251  dvfsumabs  26253  ig1peu  26403  pilem2  26691  pilem3  26692  rlimcnp2  27206  ppisval  27343  ppifi  27345  ppiprm  27390  chtprm  27392  chtdif  27397  efchtdvds  27398  ppidif  27402  ppiltx  27416  prmorcht  27417  ppiub  27443  chtlepsi  27445  pclogsum  27454  vmasum  27455  chpval2  27457  chpub  27459  2sqlem8  27665  chebbnd1lem1  27708  chtppilimlem1  27712  rpvmasum2  27751  dchrisum0re  27752  rplogsum  27766  dirith2  27767  nosupbnd1lem1  27947  nosupbnd2  27955  noinfbnd1lem1  27962  axtgcgrrflx  28806  axtgcgrid  28807  axtgsegcon  28808  axtg5seg  28809  axtgbtwnid  28810  axtgpasch  28811  axtgcont1  28812  phnv  31298  minvecolem2  31359  minvecolem3  31360  minvecolem5  31365  minvecolem6  31366  minvecolem7  31367  hlimcaui  31720  chdmm1i  31961  chabs1  32000  chabs2  32001  ledii  32020  lejdii  32022  pjoml4i  32071  cmbr3i  32084  cmbr4i  32085  cmm1i  32090  osumcor2i  32128  3oalem4  32149  pjssmii  32165  pjocini  32182  pjini  32183  mayete3i  32212  riesz4  32548  riesz1  32549  cnlnadjeui  32561  cnlnadjeu  32562  cnlnssadj  32564  nmopadjlei  32572  pjin1i  32676  pjclem1  32679  stji1i  32726  stm1i  32727  dmdbr2  32787  ssmd1  32795  mdslj2i  32804  mdsl2bi  32807  mdslmd1lem1  32809  mdslmd2i  32814  atomli  32866  atcvat4i  32881  sumdmdlem2  32903  dmdbr5ati  32906  dmdbr6ati  32907  dmdbr7ati  32908  indifbi  32998  disjxpin  33064  imadifxp  33077  nfpconfp  33108  off2  33117  ffsrn  33202  indsumin  33310  indf1ofs  33315  gsummptres  33495  xrge0tsmsd  33516  idlinsubrg  33862  ordtrestNEW  34434  qqhnm  34503  qqhcn  34504  rrhre  34534  esumval  34559  esumel  34560  gsumesum  34572  esumlub  34573  esumcst  34576  esumfsup  34583  esumpcvgval  34591  esumcvg  34599  sigainb  34650  ldgenpisyslem1  34677  measinb2  34737  sibfinima  34853  sibfof  34854  eulerpartlemelr  34871  eulerpartlem1  34881  eulerpartgbij  34886  eulerpartlemgu  34891  eulerpartlemgs2  34894  sseqf  34906  ballotlemfelz  35005  ballotlemfp1  35006  reprinrn  35129  reprinfz1  35133  hgt750lemd  35159  bnj1292  35327  connpconn  35817  iccllysconn  35832  cvmsss2  35856  cvmcov2  35857  cvmopnlem  35860  cvmliftmolem2  35864  cvmliftlem15  35880  cvmlift2lem12  35896  mvrsfpw  36088  msrf  36124  elmsta  36130  mthmpps  36164  nepss  36300  dfon2lem4  36366  txpss3v  36458  fixssdm  36486  fixssrn  36487  limitssson  36491  fneer  36975  neibastop1  36981  neibastop2lem  36982  filnetlem3  37002  ontopbas  37050  bj-disj2r  37775  bj-restpw  37845  bj-discrmoore  37864  bj-idres  37915  bj-fvsnun2  38011  bj-ablssgrp  38031  bj-fldssdrng  38043  taupilemrplb  38075  taupilem2  38077  taupi  38078  ptrest  38371  poimirlem29  38401  mblfinlem3  38411  mblfinlem4  38412  ismblfin  38413  mbfposadd  38419  sstotbnd2  38527  ssbnd  38541  heibor1lem  38562  heiborlem1  38564  heiborlem3  38566  heiborlem5  38568  heiborlem6  38569  heiborlem10  38573  heibor  38574  opidonOLD  38605  exidcl  38629  flddivrng  38752  iss2  39095  xrnss3v  39132  refrelsredund2  39468  lshpinN  39865  lcvexchlem5  39914  pmodlem2  40723  pmod1i  40724  pmodN  40726  osumcllem7N  40838  pexmidlem4N  40849  pl42lem3N  40857  djaclN  42012  dihoml4c  42252  dochdmj1  42266  djhcl  42276  dochexmidlem4  42339  mapd1o  42524  mapdin  42538  unitscyglem5  43068  redvmptabs  43238  elrfi  43542  elrfirn  43543  elrfirn2  43544  ismrcd1  43546  istopclsd  43548  isnacs2  43554  mrefg3  43556  isnacs3  43558  diophrw  43607  diophin  43620  aomclem2  43899  islmodfg  43913  lsmfgcl  43918  lmhmfgima  43928  lmhmfgsplit  43930  lmhmlnmsplit  43931  pwfi2f1o  43940  hbt  43974  ofoafg  44198  harval3  44381  elinintrab  44420  trrelind  44508  clsk3nimkb  44883  isotone2  44892  ismnushort  45128  onfrALTlem2  45372  onfrALTlem2VD  45714  wfac8prim  45828  unirestss  45959  inmap  46042  fsumiunss  46408  islptre  46452  sumnnodd  46463  limclner  46482  liminfval4  46620  liminfval3  46621  cnrefiisplem  46660  cncfuni  46717  ismbl3  46817  ismbl4  46824  fouriersw  47062  qndenserrnbllem  47125  salincl  47155  salgencntex  47174  sge0less  47223  sge0resplit  47237  sge0split  47240  sge0iunmptlemre  47246  carageniuncllem1  47352  carageniuncllem2  47353  caragenel2d  47363  hspmbllem3  47459  hspmbl  47460  ovolval2lem  47474  sssmf  47569  smfaddlem1  47594  smflimlem2  47603  smflimlem3  47604  smflimlem4  47605  smfres  47621  smfmullem4  47625  smfsuplem1  47642  wrddrin  47718  chndrin  47723  chnrrin  47728  fcoreslem2  47955  indprmfz  48536  ppivalnn  48538  rngcrescrhmALTV  49198  rhmsubcALTVlem1  49199  funcringcsetcALTV2lem9  49216  fldcALTV  49250  fldhmsubcALTV  49251  iscnrm3llem2  49879  uptrlem1  50139  uptrlem2  50140  uptrlem3  50141  uptra  50144  uptrar  50145  uobeqw  50148  uptr2  50150  uptr2a  50151  fucoppcfunc  50341  setrec2fun  50621