Theorem inss1 4184

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

Syntax hints:   ∩ cin 3898   ⊆ wss 3899

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 3435  df-in 3906  df-ss 3916

This theorem is referenced by:  inss2  4185  ssinss1  4193  unabs  4212  nssinpss  4214  dfin4  4225  inv1  4345  disjdif  4419  ifssun  4490  uniintsn  4932  wefrc  5607  relin1  5749  resss  5946  resmpt3  5983  cnvcnvss  6137  resdmss  6178  resssxp  6212  predss  6251  ordtri3or  6333  onfr  6340  ordelinel  6404  funin  6552  funimass2  6559  fnresin1  6601  fnres  6603  fresin  6687  fresaun  6689  nfvres  6854  ssimaex  6901  fneqeql2  6974  fnfvimad  7162  funiunfv  7176  isoini2  7267  ofrfvalg  7612  ofval  7615  ofrval  7616  off  7622  ofres  7623  ofco  7629  fparlem3  8038  fparlem4  8039  frrlem4  8213  frrlem13  8222  smores  8266  smores2  8268  tfrlem5  8293  pmresg  8788  sbthlem7  9000  sbthcl  9006  infi  9148  imafi  9193  ixpfi2  9228  unifpw  9233  elfiun  9308  dffi3  9309  marypha1lem  9311  ordtypelem6  9403  ordtypelem7  9404  ordtypelem8  9405  wdomima2g  9466  frmin  9633  frrlem15  9641  frrlem16  9642  tskwe  9834  ackbij1lem15  10115  ackbij1lem16  10116  fin23lem23  10208  fin23lem22  10209  fin23lem19  10218  brdom3  10410  brdom5  10411  brdom4  10412  imadomg  10416  fpwwe2lem11  10523  canthp1lem2  10535  wunin  10595  tskin  10641  gruima  10684  ingru  10697  gruina  10700  grur1a  10701  nqerf  10812  nqerrel  10814  hashun3  14279  hashin  14306  hashdif  14308  xptrrel  14874  rexanuz  15240  limsupgle  15371  rlimres  15452  lo1res  15453  lo1resb  15458  rlimresb  15459  o1resb  15460  lo1eq  15462  rlimeq  15463  o1of2  15507  o1rlimmul  15513  isercolllem2  15560  isercolllem3  15561  isercoll  15562  incexclem  15730  incexc  15731  bitsinvp1  16347  sadcaddlem  16355  sadadd2lem  16357  sadadd3  16359  sadaddlem  16364  sadasslem  16368  sadeq  16370  bitsres  16371  smuval2  16380  smupval  16386  smueqlem  16388  smumul  16391  ramub2  16913  ramub1lem2  16926  fvsetsid  17066  ressbasss2  17139  ressinbas  17143  ressress  17145  submre  17494  isacs1i  17550  mreacs  17551  acsfn  17552  invss  17655  sscres  17717  catcisolem  18004  catciso  18005  isacs5lem  18438  psss  18473  tsrss  18482  tsrdir  18497  sylow2a  19485  lsmmod  19541  gsumzres  19775  gsumzaddlem  19787  dprddisj2  19907  ablfac1eu  19941  isunit  20245  rngcbas  20490  rngchomfval  20491  rngccofval  20495  dfrngc2  20497  rnghmsscmap2  20498  rnghmsscmap  20499  rngcsect  20505  funcrngcsetc  20509  ringcbas  20519  ringchomfval  20520  ringccofval  20524  dfringc2  20526  rhmsscmap2  20527  rhmsscmap  20528  rhmsscrnghm  20534  ringcsect  20539  funcringcsetc  20543  rngcrescrhm  20553  rhmsubclem1  20554  fldc  20653  fldhmsubc  20654  acsfn1p  20668  lspextmo  20944  2idlval  21142  pjfval  21597  pjpm  21599  aspsubrg  21767  psrbagsn  21952  ofco2  22320  basdif0  22822  tgval2  22825  eltg3  22831  tgcl  22838  tgdom  22847  tgidm  22849  ppttop  22876  epttop  22878  ntropn  22918  ntrin  22930  mretopd  22961  neiptoptop  23000  restfpw  23048  neitr  23049  restcls  23050  cncls  23143  cnpresti  23157  cnprest  23158  cmpsublem  23268  cmpsub  23269  fiuncmp  23273  indisconn  23287  connsub  23290  iunconnlem  23296  islly2  23353  cldllycmp  23364  kgentopon  23407  ptbasfi  23450  ptcnplem  23490  txcnmpt  23493  txcmplem2  23511  hausdiag  23514  txkgen  23521  xkococnlem  23528  qtoptop2  23568  basqtop  23580  fbssfi  23706  filin  23723  infil  23732  fbasrn  23753  fgtr  23759  ufprim  23778  flimrest  23852  txflf  23875  fclsrest  23893  alexsubALTlem4  23919  tsmsres  24013  tsmsxplem1  24022  ustund  24091  trust  24098  utoptop  24103  restutop  24106  cfiluweak  24163  xmetres  24233  metres  24234  blin2  24298  setsmstopn  24347  metrest  24393  ressxms  24394  tgioo  24665  xrsmopn  24682  reconnlem1  24696  xrge0tsms  24704  tcphcph  25118  cfilresi  25176  cfilres  25177  caussi  25178  causs  25179  relcmpcmet  25199  minveclem4a  25311  ismbl2  25409  cmmbl  25416  nulmbl2  25418  unmbl  25419  shftmbl  25420  volinun  25428  voliunlem1  25432  voliunlem2  25433  ioombl1lem4  25443  ioombl1  25444  uniioombllem2  25465  uniioombllem3  25467  uniioombllem4  25468  uniioombllem5  25469  uniioombl  25471  volivth  25489  vitalilem3  25492  vitalilem4  25493  vitalilem5  25494  vitali  25495  mbfadd  25543  mbfsub  25544  i1fadd  25577  itg1addlem2  25579  itg1addlem4  25581  itg1addlem5  25582  itg1climres  25596  mbfmul  25608  itg2splitlem  25630  itg2split  25631  limcresi  25767  limciun  25776  dvreslem  25791  dvres2lem  25792  dvres  25793  dvres3a  25796  dvaddbr  25821  dvmulbr  25822  dvmulbrOLD  25823  dvfsumle  25907  dvfsumleOLD  25908  dvfsumabs  25910  ig1peu  26061  pilem2  26343  pilem3  26344  rlimcnp2  26857  ppisval  26995  ppifi  26997  ppiprm  27042  chtprm  27044  chtdif  27049  efchtdvds  27050  ppidif  27054  ppiltx  27068  prmorcht  27069  ppiub  27096  chtlepsi  27098  pclogsum  27107  vmasum  27108  chpval2  27110  chpub  27112  2sqlem8  27318  chebbnd1lem1  27361  chtppilimlem1  27365  rpvmasum2  27404  dchrisum0re  27405  rplogsum  27419  dirith2  27420  nosupbnd1lem1  27601  nosupbnd2  27609  noinfbnd1lem1  27616  axtgcgrrflx  28394  axtgcgrid  28395  axtgsegcon  28396  axtg5seg  28397  axtgbtwnid  28398  axtgpasch  28399  axtgcont1  28400  phnv  30745  minvecolem2  30806  minvecolem3  30807  minvecolem5  30812  minvecolem6  30813  minvecolem7  30814  hlimcaui  31167  chdmm1i  31408  chabs1  31447  chabs2  31448  ledii  31467  lejdii  31469  pjoml4i  31518  cmbr3i  31531  cmbr4i  31532  cmm1i  31537  osumcor2i  31575  3oalem4  31596  pjssmii  31612  pjocini  31629  pjini  31630  mayete3i  31659  riesz4  31995  riesz1  31996  cnlnadjeui  32008  cnlnadjeu  32009  cnlnssadj  32011  nmopadjlei  32019  pjin1i  32123  pjclem1  32126  stji1i  32173  stm1i  32174  dmdbr2  32234  ssmd1  32242  mdslj2i  32251  mdsl2bi  32254  mdslmd1lem1  32256  mdslmd2i  32261  atomli  32313  atcvat4i  32328  sumdmdlem2  32350  dmdbr5ati  32353  dmdbr6ati  32354  dmdbr7ati  32355  indifbi  32452  disjxpin  32520  imadifxp  32533  nfpconfp  32566  off2  32575  ffsrn  32663  indsumin  32798  indf1ofs  32802  gsummptres  33000  xrge0tsmsd  33010  idlinsubrg  33364  ordtrestNEW  33902  qqhnm  33971  qqhcn  33972  rrhre  34002  esumval  34027  esumel  34028  gsumesum  34040  esumlub  34041  esumcst  34044  esumfsup  34051  esumpcvgval  34059  esumcvg  34067  sigainb  34117  ldgenpisyslem1  34144  measinb2  34204  sibfinima  34320  sibfof  34321  eulerpartlemelr  34338  eulerpartlem1  34348  eulerpartgbij  34353  eulerpartlemgu  34358  eulerpartlemgs2  34361  sseqf  34373  ballotlemfelz  34472  ballotlemfp1  34473  reprinrn  34599  reprinfz1  34603  hgt750lemd  34629  bnj1292  34795  connpconn  35225  iccllysconn  35240  cvmsss2  35264  cvmcov2  35265  cvmopnlem  35268  cvmliftmolem2  35272  cvmliftlem15  35288  cvmlift2lem12  35304  mvrsfpw  35496  msrf  35532  elmsta  35538  mthmpps  35572  nepss  35708  dfon2lem4  35777  txpss3v  35869  fixssdm  35897  fixssrn  35898  limitssson  35902  fneer  36344  neibastop1  36350  neibastop2lem  36351  filnetlem3  36371  ontopbas  36419  bj-disj2r  37019  bj-restpw  37083  bj-discrmoore  37102  bj-idres  37151  bj-fvsnun2  37247  bj-ablssgrp  37267  bj-fldssdrng  37279  taupilemrplb  37311  taupilem2  37313  taupi  37314  ptrest  37616  poimirlem29  37646  mblfinlem3  37656  mblfinlem4  37657  ismblfin  37658  mbfposadd  37664  sstotbnd2  37771  ssbnd  37785  heibor1lem  37806  heiborlem1  37808  heiborlem3  37810  heiborlem5  37812  heiborlem6  37813  heiborlem10  37817  heibor  37818  opidonOLD  37849  exidcl  37873  flddivrng  37996  iss2  38329  xrnss3v  38357  refrelsredund2  38627  lshpinN  38985  lcvexchlem5  39034  pmodlem2  39843  pmod1i  39844  pmodN  39846  osumcllem7N  39958  pexmidlem4N  39969  pl42lem3N  39977  djaclN  41132  dihoml4c  41372  dochdmj1  41386  djhcl  41396  dochexmidlem4  41459  mapd1o  41644  mapdin  41658  unitscyglem5  42189  redvmptabs  42350  elrfi  42684  elrfirn  42685  elrfirn2  42686  ismrcd1  42688  istopclsd  42690  isnacs2  42696  mrefg3  42698  isnacs3  42700  diophrw  42749  diophin  42762  aomclem2  43045  islmodfg  43059  lsmfgcl  43064  lmhmfgima  43074  lmhmfgsplit  43076  lmhmlnmsplit  43077  pwfi2f1o  43086  hbt  43120  ofoafg  43344  harval3  43528  elinintrab  43567  trrelind  43655  clsk3nimkb  44030  isotone2  44039  ismnushort  44291  onfrALTlem2  44536  onfrALTlem2VD  44878  wfac8prim  44992  unirestss  45118  inmap  45203  fsumiunss  45572  islptre  45616  sumnnodd  45627  limclner  45646  liminfval4  45784  liminfval3  45785  cnrefiisplem  45824  cncfuni  45881  ismbl3  45981  ismbl4  45988  fouriersw  46226  qndenserrnbllem  46289  salincl  46319  salgencntex  46338  sge0less  46387  sge0resplit  46401  sge0split  46404  sge0iunmptlemre  46410  carageniuncllem1  46516  carageniuncllem2  46517  caragenel2d  46527  hspmbllem3  46623  hspmbl  46624  ovolval2lem  46638  sssmf  46733  smfaddlem1  46758  smflimlem2  46767  smflimlem3  46768  smflimlem4  46769  smfres  46785  smfmullem4  46789  smfsuplem1  46806  fcoreslem2  47062  rngcrescrhmALTV  48278  rhmsubcALTVlem1  48279  funcringcsetcALTV2lem9  48296  fldcALTV  48330  fldhmsubcALTV  48331  iscnrm3llem2  48948  uptrlem1  49209  uptrlem2  49210  uptrlem3  49211  uptra  49214  uptrar  49215  uobeqw  49218  uptr2  49220  uptr2a  49221  fucoppcfunc  49411  setrec2fun  49691