Theorem inss1 4237

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

Syntax hints:   ∩ cin 3950   ⊆ wss 3951

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  inss2  4238  ssinss1  4246  unabs  4265  nssinpss  4267  dfin4  4278  inv1  4398  disjdif  4472  ifssun  4543  uniintsn  4985  wefrc  5679  relin1  5822  resss  6019  resmpt3  6056  cnvcnvss  6214  resdmss  6255  resssxp  6290  predss  6329  ordtri3or  6416  onfr  6423  ordelinel  6485  funin  6642  funimass2  6649  fnresin1  6693  fnres  6695  fresin  6777  fresaun  6779  nfvres  6947  ssimaex  6994  fneqeql2  7067  fnfvimad  7254  funiunfv  7268  isoini2  7359  ofrfvalg  7705  ofval  7708  ofrval  7709  off  7715  ofres  7716  ofco  7722  fparlem3  8139  fparlem4  8140  frrlem4  8314  frrlem13  8323  smores  8392  smores2  8394  tfrlem5  8420  pmresg  8910  sbthlem7  9129  sbthcl  9135  infi  9302  imafi  9353  ixpfi2  9390  unifpw  9395  elfiun  9470  dffi3  9471  marypha1lem  9473  ordtypelem6  9563  ordtypelem7  9564  ordtypelem8  9565  wdomima2g  9626  frmin  9789  frrlem15  9797  frrlem16  9798  tskwe  9990  ackbij1lem15  10273  ackbij1lem16  10274  fin23lem23  10366  fin23lem22  10367  fin23lem19  10376  brdom3  10568  brdom5  10569  brdom4  10570  imadomg  10574  fpwwe2lem11  10681  canthp1lem2  10693  wunin  10753  tskin  10799  gruima  10842  ingru  10855  gruina  10858  grur1a  10859  nqerf  10970  nqerrel  10972  hashun3  14423  hashin  14450  hashdif  14452  xptrrel  15019  rexanuz  15384  limsupgle  15513  rlimres  15594  lo1res  15595  lo1resb  15600  rlimresb  15601  o1resb  15602  lo1eq  15604  rlimeq  15605  o1of2  15649  o1rlimmul  15655  isercolllem2  15702  isercolllem3  15703  isercoll  15704  incexclem  15872  incexc  15873  bitsinvp1  16486  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadaddlem  16503  sadasslem  16507  sadeq  16509  bitsres  16510  smuval2  16519  smupval  16525  smueqlem  16527  smumul  16530  ramub2  17052  ramub1lem2  17065  fvsetsid  17205  ressbasss2  17286  ressinbas  17291  ressress  17293  submre  17648  isacs1i  17700  mreacs  17701  acsfn  17702  invss  17805  sscres  17867  catcisolem  18155  catciso  18156  isacs5lem  18590  psss  18625  tsrss  18634  tsrdir  18649  sylow2a  19637  lsmmod  19693  gsumzres  19927  gsumzaddlem  19939  dprddisj2  20059  ablfac1eu  20093  isunit  20373  rngcbas  20621  rngchomfval  20622  rngccofval  20626  dfrngc2  20628  rnghmsscmap2  20629  rnghmsscmap  20630  rngcsect  20636  funcrngcsetc  20640  ringcbas  20650  ringchomfval  20651  ringccofval  20655  dfringc2  20657  rhmsscmap2  20658  rhmsscmap  20659  rhmsscrnghm  20665  ringcsect  20670  funcringcsetc  20674  rngcrescrhm  20684  rhmsubclem1  20685  fldc  20785  fldhmsubc  20786  acsfn1p  20800  lspextmo  21055  2idlval  21261  pjfval  21726  pjpm  21728  aspsubrg  21896  psrbagsn  22087  ofco2  22457  basdif0  22960  tgval2  22963  eltg3  22969  tgcl  22976  tgdom  22985  tgidm  22987  ppttop  23014  epttop  23016  ntropn  23057  ntrin  23069  mretopd  23100  neiptoptop  23139  restfpw  23187  neitr  23188  restcls  23189  cncls  23282  cnpresti  23296  cnprest  23297  cmpsublem  23407  cmpsub  23408  fiuncmp  23412  indisconn  23426  connsub  23429  iunconnlem  23435  islly2  23492  cldllycmp  23503  kgentopon  23546  ptbasfi  23589  ptcnplem  23629  txcnmpt  23632  txcmplem2  23650  hausdiag  23653  txkgen  23660  xkococnlem  23667  qtoptop2  23707  basqtop  23719  fbssfi  23845  filin  23862  infil  23871  fbasrn  23892  fgtr  23898  ufprim  23917  flimrest  23991  txflf  24014  fclsrest  24032  alexsubALTlem4  24058  tsmsres  24152  tsmsxplem1  24161  ustund  24230  trust  24238  utoptop  24243  restutop  24246  cfiluweak  24304  xmetres  24374  metres  24375  blin2  24439  setsmstopn  24490  metrest  24537  ressxms  24538  tgioo  24817  xrsmopn  24834  reconnlem1  24848  xrge0tsms  24856  tcphcph  25271  cfilresi  25329  cfilres  25330  caussi  25331  causs  25332  relcmpcmet  25352  minveclem4a  25464  ismbl2  25562  cmmbl  25569  nulmbl2  25571  unmbl  25572  shftmbl  25573  volinun  25581  voliunlem1  25585  voliunlem2  25586  ioombl1lem4  25596  ioombl1  25597  uniioombllem2  25618  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombl  25624  volivth  25642  vitalilem3  25645  vitalilem4  25646  vitalilem5  25647  vitali  25648  mbfadd  25696  mbfsub  25697  i1fadd  25730  itg1addlem2  25732  itg1addlem4  25734  itg1addlem5  25735  itg1climres  25749  mbfmul  25761  itg2splitlem  25783  itg2split  25784  limcresi  25920  limciun  25929  dvreslem  25944  dvres2lem  25945  dvres  25946  dvres3a  25949  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  ig1peu  26214  pilem2  26496  pilem3  26497  rlimcnp2  27009  ppisval  27147  ppifi  27149  ppiprm  27194  chtprm  27196  chtdif  27201  efchtdvds  27202  ppidif  27206  ppiltx  27220  prmorcht  27221  ppiub  27248  chtlepsi  27250  pclogsum  27259  vmasum  27260  chpval2  27262  chpub  27264  2sqlem8  27470  chebbnd1lem1  27513  chtppilimlem1  27517  rpvmasum2  27556  dchrisum0re  27557  rplogsum  27571  dirith2  27572  nosupbnd1lem1  27753  nosupbnd2  27761  noinfbnd1lem1  27768  axtgcgrrflx  28470  axtgcgrid  28471  axtgsegcon  28472  axtg5seg  28473  axtgbtwnid  28474  axtgpasch  28475  axtgcont1  28476  phnv  30833  minvecolem2  30894  minvecolem3  30895  minvecolem5  30900  minvecolem6  30901  minvecolem7  30902  hlimcaui  31255  chdmm1i  31496  chabs1  31535  chabs2  31536  ledii  31555  lejdii  31557  pjoml4i  31606  cmbr3i  31619  cmbr4i  31620  cmm1i  31625  osumcor2i  31663  3oalem4  31684  pjssmii  31700  pjocini  31717  pjini  31718  mayete3i  31747  riesz4  32083  riesz1  32084  cnlnadjeui  32096  cnlnadjeu  32097  cnlnssadj  32099  nmopadjlei  32107  pjin1i  32211  pjclem1  32214  stji1i  32261  stm1i  32262  dmdbr2  32322  ssmd1  32330  mdslj2i  32339  mdsl2bi  32342  mdslmd1lem1  32344  mdslmd2i  32349  atomli  32401  atcvat4i  32416  sumdmdlem2  32438  dmdbr5ati  32441  dmdbr6ati  32442  dmdbr7ati  32443  indifbi  32539  disjxpin  32601  imadifxp  32614  nfpconfp  32642  off2  32651  ffsrn  32740  indsumin  32847  indf1ofs  32851  gsummptres  33055  xrge0tsmsd  33065  idlinsubrg  33459  ordtrestNEW  33920  qqhnm  33991  qqhcn  33992  rrhre  34022  esumval  34047  esumel  34048  gsumesum  34060  esumlub  34061  esumcst  34064  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  sigainb  34137  ldgenpisyslem1  34164  measinb2  34224  sibfinima  34341  sibfof  34342  eulerpartlemelr  34359  eulerpartlem1  34369  eulerpartgbij  34374  eulerpartlemgu  34379  eulerpartlemgs2  34382  sseqf  34394  ballotlemfelz  34493  ballotlemfp1  34494  reprinrn  34633  reprinfz1  34637  hgt750lemd  34663  bnj1292  34829  connpconn  35240  iccllysconn  35255  cvmsss2  35279  cvmcov2  35280  cvmopnlem  35283  cvmliftmolem2  35287  cvmliftlem15  35303  cvmlift2lem12  35319  mvrsfpw  35511  msrf  35547  elmsta  35553  mthmpps  35587  nepss  35718  dfon2lem4  35787  txpss3v  35879  fixssdm  35907  fixssrn  35908  limitssson  35912  fneer  36354  neibastop1  36360  neibastop2lem  36361  filnetlem3  36381  ontopbas  36429  bj-disj2r  37029  bj-restpw  37093  bj-discrmoore  37112  bj-idres  37161  bj-fvsnun2  37257  bj-ablssgrp  37277  bj-fldssdrng  37289  taupilemrplb  37321  taupilem2  37323  taupi  37324  ptrest  37626  poimirlem29  37656  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  mbfposadd  37674  sstotbnd2  37781  ssbnd  37795  heibor1lem  37816  heiborlem1  37818  heiborlem3  37820  heiborlem5  37822  heiborlem6  37823  heiborlem10  37827  heibor  37828  opidonOLD  37859  exidcl  37883  flddivrng  38006  iss2  38345  xrnss3v  38373  refrelsredund2  38634  lshpinN  38990  lcvexchlem5  39039  pmodlem2  39849  pmod1i  39850  pmodN  39852  osumcllem7N  39964  pexmidlem4N  39975  pl42lem3N  39983  djaclN  41138  dihoml4c  41378  dochdmj1  41392  djhcl  41402  dochexmidlem4  41465  mapd1o  41650  mapdin  41664  unitscyglem5  42200  redvmptabs  42390  elrfi  42705  elrfirn  42706  elrfirn2  42707  ismrcd1  42709  istopclsd  42711  isnacs2  42717  mrefg3  42719  isnacs3  42721  diophrw  42770  diophin  42783  aomclem2  43067  islmodfg  43081  lsmfgcl  43086  lmhmfgima  43096  lmhmfgsplit  43098  lmhmlnmsplit  43099  pwfi2f1o  43108  hbt  43142  ofoafg  43367  harval3  43551  elinintrab  43590  trrelind  43678  clsk3nimkb  44053  isotone2  44062  ismnushort  44320  onfrALTlem2  44566  onfrALTlem2VD  44909  wfac8prim  45019  unirestss  45129  inmap  45214  fsumiunss  45590  islptre  45634  sumnnodd  45645  limclner  45666  liminfval4  45804  liminfval3  45805  cnrefiisplem  45844  cncfuni  45901  ismbl3  46001  ismbl4  46008  fouriersw  46246  qndenserrnbllem  46309  salincl  46339  salgencntex  46358  sge0less  46407  sge0resplit  46421  sge0split  46424  sge0iunmptlemre  46430  carageniuncllem1  46536  carageniuncllem2  46537  caragenel2d  46547  hspmbllem3  46643  hspmbl  46644  ovolval2lem  46658  sssmf  46753  smfaddlem1  46778  smflimlem2  46787  smflimlem3  46788  smflimlem4  46789  smfres  46805  smfmullem4  46809  smfsuplem1  46826  fcoreslem2  47076  rngcrescrhmALTV  48196  rhmsubcALTVlem1  48197  funcringcsetcALTV2lem9  48214  fldcALTV  48248  fldhmsubcALTV  48249  iscnrm3llem2  48847  setrec2fun  49211