Theorem inss1 4212

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

Syntax hints:   ∩ cin 3925   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  inss2  4213  ssinss1  4221  unabs  4240  nssinpss  4242  dfin4  4253  inv1  4373  disjdif  4447  ifssun  4518  uniintsn  4961  wefrc  5648  relin1  5791  resss  5988  resmpt3  6025  cnvcnvss  6183  resdmss  6224  resssxp  6259  predss  6298  ordtri3or  6384  onfr  6391  ordelinel  6454  funin  6611  funimass2  6618  fnresin1  6662  fnres  6664  fresin  6746  fresaun  6748  nfvres  6916  ssimaex  6963  fneqeql2  7036  fnfvimad  7225  funiunfv  7239  isoini2  7331  ofrfvalg  7677  ofval  7680  ofrval  7681  off  7687  ofres  7688  ofco  7694  fparlem3  8111  fparlem4  8112  frrlem4  8286  frrlem13  8295  smores  8364  smores2  8366  tfrlem5  8392  pmresg  8882  sbthlem7  9101  sbthcl  9107  infi  9272  imafi  9323  ixpfi2  9360  unifpw  9365  elfiun  9440  dffi3  9441  marypha1lem  9443  ordtypelem6  9535  ordtypelem7  9536  ordtypelem8  9537  wdomima2g  9598  frmin  9761  frrlem15  9769  frrlem16  9770  tskwe  9962  ackbij1lem15  10245  ackbij1lem16  10246  fin23lem23  10338  fin23lem22  10339  fin23lem19  10348  brdom3  10540  brdom5  10541  brdom4  10542  imadomg  10546  fpwwe2lem11  10653  canthp1lem2  10665  wunin  10725  tskin  10771  gruima  10814  ingru  10827  gruina  10830  grur1a  10831  nqerf  10942  nqerrel  10944  hashun3  14400  hashin  14427  hashdif  14429  xptrrel  14997  rexanuz  15362  limsupgle  15491  rlimres  15572  lo1res  15573  lo1resb  15578  rlimresb  15579  o1resb  15580  lo1eq  15582  rlimeq  15583  o1of2  15627  o1rlimmul  15633  isercolllem2  15680  isercolllem3  15681  isercoll  15682  incexclem  15850  incexc  15851  bitsinvp1  16466  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  sadasslem  16487  sadeq  16489  bitsres  16490  smuval2  16499  smupval  16505  smueqlem  16507  smumul  16510  ramub2  17032  ramub1lem2  17045  fvsetsid  17185  ressbasss2  17260  ressinbas  17264  ressress  17266  submre  17615  isacs1i  17667  mreacs  17668  acsfn  17669  invss  17772  sscres  17834  catcisolem  18121  catciso  18122  isacs5lem  18553  psss  18588  tsrss  18597  tsrdir  18612  sylow2a  19598  lsmmod  19654  gsumzres  19888  gsumzaddlem  19900  dprddisj2  20020  ablfac1eu  20054  isunit  20331  rngcbas  20579  rngchomfval  20580  rngccofval  20584  dfrngc2  20586  rnghmsscmap2  20587  rnghmsscmap  20588  rngcsect  20594  funcrngcsetc  20598  ringcbas  20608  ringchomfval  20609  ringccofval  20613  dfringc2  20615  rhmsscmap2  20616  rhmsscmap  20617  rhmsscrnghm  20623  ringcsect  20628  funcringcsetc  20632  rngcrescrhm  20642  rhmsubclem1  20643  fldc  20742  fldhmsubc  20743  acsfn1p  20757  lspextmo  21012  2idlval  21210  pjfval  21664  pjpm  21666  aspsubrg  21834  psrbagsn  22019  ofco2  22387  basdif0  22889  tgval2  22892  eltg3  22898  tgcl  22905  tgdom  22914  tgidm  22916  ppttop  22943  epttop  22945  ntropn  22985  ntrin  22997  mretopd  23028  neiptoptop  23067  restfpw  23115  neitr  23116  restcls  23117  cncls  23210  cnpresti  23224  cnprest  23225  cmpsublem  23335  cmpsub  23336  fiuncmp  23340  indisconn  23354  connsub  23357  iunconnlem  23363  islly2  23420  cldllycmp  23431  kgentopon  23474  ptbasfi  23517  ptcnplem  23557  txcnmpt  23560  txcmplem2  23578  hausdiag  23581  txkgen  23588  xkococnlem  23595  qtoptop2  23635  basqtop  23647  fbssfi  23773  filin  23790  infil  23799  fbasrn  23820  fgtr  23826  ufprim  23845  flimrest  23919  txflf  23942  fclsrest  23960  alexsubALTlem4  23986  tsmsres  24080  tsmsxplem1  24089  ustund  24158  trust  24166  utoptop  24171  restutop  24174  cfiluweak  24231  xmetres  24301  metres  24302  blin2  24366  setsmstopn  24415  metrest  24461  ressxms  24462  tgioo  24733  xrsmopn  24750  reconnlem1  24764  xrge0tsms  24772  tcphcph  25187  cfilresi  25245  cfilres  25246  caussi  25247  causs  25248  relcmpcmet  25268  minveclem4a  25380  ismbl2  25478  cmmbl  25485  nulmbl2  25487  unmbl  25488  shftmbl  25489  volinun  25497  voliunlem1  25501  voliunlem2  25502  ioombl1lem4  25512  ioombl1  25513  uniioombllem2  25534  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  uniioombl  25540  volivth  25558  vitalilem3  25561  vitalilem4  25562  vitalilem5  25563  vitali  25564  mbfadd  25612  mbfsub  25613  i1fadd  25646  itg1addlem2  25648  itg1addlem4  25650  itg1addlem5  25651  itg1climres  25665  mbfmul  25677  itg2splitlem  25699  itg2split  25700  limcresi  25836  limciun  25845  dvreslem  25860  dvres2lem  25861  dvres  25862  dvres3a  25865  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  ig1peu  26130  pilem2  26412  pilem3  26413  rlimcnp2  26926  ppisval  27064  ppifi  27066  ppiprm  27111  chtprm  27113  chtdif  27118  efchtdvds  27119  ppidif  27123  ppiltx  27137  prmorcht  27138  ppiub  27165  chtlepsi  27167  pclogsum  27176  vmasum  27177  chpval2  27179  chpub  27181  2sqlem8  27387  chebbnd1lem1  27430  chtppilimlem1  27434  rpvmasum2  27473  dchrisum0re  27474  rplogsum  27488  dirith2  27489  nosupbnd1lem1  27670  nosupbnd2  27678  noinfbnd1lem1  27685  axtgcgrrflx  28387  axtgcgrid  28388  axtgsegcon  28389  axtg5seg  28390  axtgbtwnid  28391  axtgpasch  28392  axtgcont1  28393  phnv  30741  minvecolem2  30802  minvecolem3  30803  minvecolem5  30808  minvecolem6  30809  minvecolem7  30810  hlimcaui  31163  chdmm1i  31404  chabs1  31443  chabs2  31444  ledii  31463  lejdii  31465  pjoml4i  31514  cmbr3i  31527  cmbr4i  31528  cmm1i  31533  osumcor2i  31571  3oalem4  31592  pjssmii  31608  pjocini  31625  pjini  31626  mayete3i  31655  riesz4  31991  riesz1  31992  cnlnadjeui  32004  cnlnadjeu  32005  cnlnssadj  32007  nmopadjlei  32015  pjin1i  32119  pjclem1  32122  stji1i  32169  stm1i  32170  dmdbr2  32230  ssmd1  32238  mdslj2i  32247  mdsl2bi  32250  mdslmd1lem1  32252  mdslmd2i  32257  atomli  32309  atcvat4i  32324  sumdmdlem2  32346  dmdbr5ati  32349  dmdbr6ati  32350  dmdbr7ati  32351  indifbi  32447  disjxpin  32515  imadifxp  32528  nfpconfp  32556  off2  32565  ffsrn  32652  indsumin  32785  indf1ofs  32789  gsummptres  32992  xrge0tsmsd  33002  idlinsubrg  33392  ordtrestNEW  33898  qqhnm  33967  qqhcn  33968  rrhre  33998  esumval  34023  esumel  34024  gsumesum  34036  esumlub  34037  esumcst  34040  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  sigainb  34113  ldgenpisyslem1  34140  measinb2  34200  sibfinima  34317  sibfof  34318  eulerpartlemelr  34335  eulerpartlem1  34345  eulerpartgbij  34350  eulerpartlemgu  34355  eulerpartlemgs2  34358  sseqf  34370  ballotlemfelz  34469  ballotlemfp1  34470  reprinrn  34596  reprinfz1  34600  hgt750lemd  34626  bnj1292  34792  connpconn  35203  iccllysconn  35218  cvmsss2  35242  cvmcov2  35243  cvmopnlem  35246  cvmliftmolem2  35250  cvmliftlem15  35266  cvmlift2lem12  35282  mvrsfpw  35474  msrf  35510  elmsta  35516  mthmpps  35550  nepss  35681  dfon2lem4  35750  txpss3v  35842  fixssdm  35870  fixssrn  35871  limitssson  35875  fneer  36317  neibastop1  36323  neibastop2lem  36324  filnetlem3  36344  ontopbas  36392  bj-disj2r  36992  bj-restpw  37056  bj-discrmoore  37075  bj-idres  37124  bj-fvsnun2  37220  bj-ablssgrp  37240  bj-fldssdrng  37252  taupilemrplb  37284  taupilem2  37286  taupi  37287  ptrest  37589  poimirlem29  37619  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  mbfposadd  37637  sstotbnd2  37744  ssbnd  37758  heibor1lem  37779  heiborlem1  37781  heiborlem3  37783  heiborlem5  37785  heiborlem6  37786  heiborlem10  37790  heibor  37791  opidonOLD  37822  exidcl  37846  flddivrng  37969  iss2  38308  xrnss3v  38336  refrelsredund2  38597  lshpinN  38953  lcvexchlem5  39002  pmodlem2  39812  pmod1i  39813  pmodN  39815  osumcllem7N  39927  pexmidlem4N  39938  pl42lem3N  39946  djaclN  41101  dihoml4c  41341  dochdmj1  41355  djhcl  41365  dochexmidlem4  41428  mapd1o  41613  mapdin  41627  unitscyglem5  42158  redvmptabs  42350  elrfi  42664  elrfirn  42665  elrfirn2  42666  ismrcd1  42668  istopclsd  42670  isnacs2  42676  mrefg3  42678  isnacs3  42680  diophrw  42729  diophin  42742  aomclem2  43026  islmodfg  43040  lsmfgcl  43045  lmhmfgima  43055  lmhmfgsplit  43057  lmhmlnmsplit  43058  pwfi2f1o  43067  hbt  43101  ofoafg  43325  harval3  43509  elinintrab  43548  trrelind  43636  clsk3nimkb  44011  isotone2  44020  ismnushort  44273  onfrALTlem2  44519  onfrALTlem2VD  44861  wfac8prim  44975  unirestss  45096  inmap  45181  fsumiunss  45552  islptre  45596  sumnnodd  45607  limclner  45628  liminfval4  45766  liminfval3  45767  cnrefiisplem  45806  cncfuni  45863  ismbl3  45963  ismbl4  45970  fouriersw  46208  qndenserrnbllem  46271  salincl  46301  salgencntex  46320  sge0less  46369  sge0resplit  46383  sge0split  46386  sge0iunmptlemre  46392  carageniuncllem1  46498  carageniuncllem2  46499  caragenel2d  46509  hspmbllem3  46605  hspmbl  46606  ovolval2lem  46620  sssmf  46715  smfaddlem1  46740  smflimlem2  46749  smflimlem3  46750  smflimlem4  46751  smfres  46767  smfmullem4  46771  smfsuplem1  46788  fcoreslem2  47041  rngcrescrhmALTV  48203  rhmsubcALTVlem1  48204  funcringcsetcALTV2lem9  48221  fldcALTV  48255  fldhmsubcALTV  48256  iscnrm3llem2  48872  setrec2fun  49504