Theorem inss1 3833

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

Syntax hints:   ∩ cin 3573   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  inss2  3834  ssinss1  3841  unabs  3854  nssinpss  3856  dfin4  3867  inv1  3970  disjdif  4040  uniintsn  4514  wefrc  5108  relin1  5236  resss  5422  resmpt3  5450  cnvcnvss  5589  predss  5687  ordtri3or  5755  onfr  5763  ordelinel  5825  ordelinelOLD  5826  funin  5965  funimass2  5972  fnresin1  6005  fnres  6007  fresin  6073  fresaun  6075  fresaunres2  6076  nfvres  6224  ssimaex  6263  fneqeql2  6326  funiunfv  6506  isoini2  6589  ofrfval  6905  ofval  6906  ofrval  6907  off  6912  ofres  6913  ofco  6917  fparlem3  7279  fparlem4  7280  wfrlem4  7418  smores  7449  smores2  7451  tfrlem5  7476  pmresg  7885  sbthlem7  8076  sbthcl  8082  infi  8184  imafi  8259  ixpfi2  8264  unifpw  8269  f1opwfi  8270  fival  8318  fi0  8326  dffi2  8329  elfiun  8336  dffi3  8337  marypha1lem  8339  ordtypelem3  8425  ordtypelem4  8426  ordtypelem6  8428  ordtypelem7  8429  ordtypelem8  8430  wdomima2g  8491  epfrs  8607  tskwe  8776  r0weon  8835  fodomfi2  8883  infpwfien  8885  ackbij1lem6  9047  ackbij1lem9  9050  ackbij1lem10  9051  ackbij1lem11  9052  ackbij1lem15  9056  ackbij1lem16  9057  fin23lem24  9144  fin23lem26  9147  fin23lem23  9148  fin23lem22  9149  fin23lem19  9158  isfin1-3  9208  ttukeylem6  9336  brdom3  9350  brdom5  9351  brdom4  9352  imadomg  9356  fpwwe2lem12  9463  canthp1lem2  9475  wunin  9535  tskin  9581  gruima  9624  ingru  9637  gruina  9640  grur1a  9641  nqerf  9752  nqerrel  9754  dedekindle  10201  hashun3  13173  hashin  13199  hashdif  13201  xptrrel  13719  rexanuz  14085  limsupgle  14208  rlimres  14289  lo1res  14290  lo1resb  14295  rlimresb  14296  o1resb  14297  lo1eq  14299  rlimeq  14300  o1of2  14343  o1rlimmul  14349  isercolllem2  14396  isercolllem3  14397  isercoll  14398  ackbijnn  14560  incexclem  14568  incexc  14569  bitsinvp1  15171  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  sadeq  15194  bitsres  15195  smuval2  15204  smupval  15210  smueqlem  15212  smumul  15215  ramub2  15718  ramub1lem2  15731  fvsetsid  15890  ressinbas  15936  ressress  15938  submre  16265  submrc  16288  isacs2  16314  isacs1i  16318  mreacs  16319  acsfn  16320  invss  16421  sscres  16483  coffth  16596  catcisolem  16756  catciso  16757  catcoppccl  16758  catcfuccl  16759  catcxpccl  16847  isdrs2  16939  isacs3lem  17166  isacs5lem  17169  acsfiindd  17177  psss  17214  psssdm2  17215  tsrss  17223  tsrdir  17238  resscntz  17764  sylow2a  18034  lsmmod  18088  frgpnabllem2  18277  gsumzres  18310  gsumzaddlem  18321  dprddisj2  18438  ablfac1eu  18472  ablfac2  18488  isunit  18657  lspextmo  19056  2idlval  19233  aspsubrg  19331  psrbagsn  19495  mplind  19502  zringlpirlem2  19833  pjfval  20050  pjpm  20052  ofco2  20257  basdif0  20757  tgval2  20760  eltg3  20766  tgcl  20773  tgdom  20782  tgidm  20784  ppttop  20811  epttop  20813  ntropn  20853  ntrin  20865  mretopd  20896  mreclatdemoBAD  20900  neiptoptop  20935  restbas  20962  restfpw  20983  neitr  20984  restcls  20985  ordtrest  21006  subbascn  21058  cncls  21078  cnpresti  21092  cnprest  21093  fincmp  21196  cmpsublem  21202  cmpsub  21203  fiuncmp  21207  indisconn  21221  connsub  21224  cnconn  21225  iunconnlem  21230  clsconn  21233  conncompclo  21238  islly2  21287  cldllycmp  21298  kgentopon  21341  llycmpkgen2  21353  1stckgenlem  21356  ptbasfi  21384  txcls  21407  txcnp  21423  ptcnplem  21424  txcnmpt  21427  txcmplem2  21445  hausdiag  21448  txkgen  21455  xkopt  21458  xkococnlem  21462  txconn  21492  qtoptop2  21502  basqtop  21514  tgqtop  21515  kqnrmlem1  21546  kqnrmlem2  21547  nrmhmph  21597  fbssfi  21641  filin  21658  infil  21667  fbasrn  21688  fgtr  21694  ufprim  21713  flimrest  21787  hauspwpwf1  21791  txflf  21810  fclsrest  21828  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem5  21860  tsmsres  21947  tsmsxplem1  21956  ustund  22025  trust  22033  utoptop  22038  restutop  22041  cfiluweak  22099  xmetres  22169  metres  22170  blin2  22234  blbas  22235  blres  22236  setsmstopn  22283  met2ndci  22327  metrest  22329  ressxms  22330  tgioo  22599  xrsmopn  22615  zdis  22619  reconnlem1  22629  reconnlem2  22630  xrge0tsms  22637  cnheibor  22754  lebnum  22763  nmoleub2lem  22914  nmoleub2lem2  22916  nmhmcn  22920  tchcph  23036  cfilresi  23093  cfilres  23094  caussi  23095  causs  23096  relcmpcmet  23115  minveclem4a  23201  minveclem4  23203  ismbl2  23295  cmmbl  23302  nulmbl2  23304  unmbl  23305  shftmbl  23306  volinun  23314  voliunlem1  23318  voliunlem2  23319  ioombl1lem4  23329  ioombl1  23330  ioorcl  23345  uniioombllem2  23351  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombl  23357  volivth  23375  vitalilem3  23379  vitalilem4  23380  vitalilem5  23381  vitali  23382  mbfadd  23428  mbfsub  23429  i1fima2  23446  i1fd  23448  i1fadd  23462  itg1addlem2  23464  itg1addlem4  23466  itg1addlem5  23467  itg1climres  23481  mbfmul  23493  itg2splitlem  23515  itg2split  23516  limcresi  23649  limciun  23658  limcun  23659  dvreslem  23673  dvres2lem  23674  dvres  23675  dvres3a  23678  dvaddbr  23701  dvmulbr  23702  dvfsumle  23784  dvfsumabs  23786  ig1peu  23931  taylfvallem1  24111  pilem2  24206  pilem3  24207  rlimcnp2  24693  xrlimcnp  24695  ppisval  24830  ppifi  24832  ppiprm  24877  ppinprm  24878  chtprm  24879  chtnprm  24880  chtdif  24884  efchtdvds  24885  ppidif  24889  ppiltx  24903  prmorcht  24904  ppiub  24929  chtlepsi  24931  chtleppi  24935  pclogsum  24940  vmasum  24941  chpval2  24943  chpchtsum  24944  chpub  24945  2sqlem8  25151  chebbnd1lem1  25158  chtppilimlem1  25162  rplogsumlem2  25174  rpvmasum2  25201  dchrisum0re  25202  rplogsum  25216  dirith2  25217  axtgcgrrflx  25361  axtgcgrid  25362  axtgsegcon  25363  axtg5seg  25364  axtgbtwnid  25365  axtgpasch  25366  axtgcont1  25367  perpcom  25608  perpneq  25609  ragperp  25612  phnv  27669  minvecolem2  27731  minvecolem3  27732  minvecolem5  27737  minvecolem6  27738  minvecolem7  27739  hlimcaui  28093  chdmm1i  28336  chabs1  28375  chabs2  28376  ledii  28395  lejdii  28397  pjoml4i  28446  cmbr3i  28459  cmbr4i  28460  cmm1i  28465  osumcor2i  28503  3oalem4  28524  pjssmii  28540  pjocini  28557  pjini  28558  mayete3i  28587  riesz4  28923  riesz1  28924  cnlnadjeui  28936  cnlnadjeu  28937  cnlnssadj  28939  nmopadjlei  28947  pjin1i  29051  pjclem1  29054  stji1i  29101  stm1i  29102  dmdbr2  29162  ssmd1  29170  mdslj2i  29179  mdsl2bi  29182  mdslmd1lem1  29184  mdslmd2i  29189  atomli  29241  atcvat4i  29256  sumdmdlem2  29278  dmdbr5ati  29281  dmdbr6ati  29282  dmdbr7ati  29283  disjxpin  29401  imadifxp  29414  off2  29443  ffsrn  29504  gsummptres  29784  xrge0tsmsd  29785  ordtrestNEW  29967  qqhnm  30034  qqhcn  30035  rrhre  30065  indsumin  30084  indf1ofs  30088  esumval  30108  esumel  30109  gsumesum  30121  esumlub  30122  esumcst  30125  esumfsup  30132  esumpcvgval  30140  esumcvg  30148  sigainb  30199  ldgenpisyslem1  30226  measinb2  30286  sibfinima  30401  sibfof  30402  eulerpartlemelr  30419  eulerpartlem1  30429  eulerpartgbij  30434  eulerpartlemgu  30439  eulerpartlemgs2  30442  sseqf  30454  ballotlemfelz  30552  ballotlemfp1  30553  reprinrn  30696  reprinfz1  30700  hgt750lemd  30726  bnj1292  30886  connpconn  31217  iccllysconn  31232  cvmsss2  31256  cvmcov2  31257  cvmopnlem  31260  cvmliftmolem2  31264  cvmliftlem15  31280  cvmlift2lem12  31296  mvrsfpw  31403  msrf  31439  elmsta  31445  mthmpps  31479  nepss  31599  dfon2lem4  31691  frrlem4  31783  nosupbnd1lem1  31854  nosupbnd2  31862  txpss3v  31985  fixssdm  32013  fixssrn  32014  limitssson  32018  fneer  32348  neibastop1  32354  neibastop2lem  32355  filnetlem3  32375  ontopbas  32427  bj-disj2r  33013  bj-restpw  33045  bj-discrmoore  33066  bj-ablssgrp  33138  taupilemrplb  33166  taupilem2  33168  taupi  33169  ptrest  33408  poimirlem29  33438  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  mbfposadd  33457  sstotbnd2  33573  ssbnd  33587  heibor1lem  33608  heiborlem1  33610  heiborlem3  33612  heiborlem5  33614  heiborlem6  33615  heiborlem10  33619  heibor  33620  opidonOLD  33651  exidcl  33675  flddivrng  33798  iss2  34112  xrnss3v  34135  lshpinN  34276  lcvexchlem5  34325  pmodlem2  35133  pmod1i  35134  pmodN  35136  osumcllem7N  35248  pexmidlem4N  35259  pl42lem3N  35267  djaclN  36425  dihoml4c  36665  dochdmj1  36679  djhcl  36689  dochexmidlem4  36752  mapd1o  36937  mapdin  36951  elrfi  37257  elrfirn  37258  elrfirn2  37259  ismrcd1  37261  istopclsd  37263  isnacs2  37269  mrefg3  37271  isnacs3  37273  diophrw  37322  diophin  37336  aomclem2  37625  islmodfg  37639  lsmfgcl  37644  lmhmfgima  37654  lmhmfgsplit  37656  lmhmlnmsplit  37657  pwfi2f1o  37666  hbt  37700  acsfn1p  37769  elinintrab  37883  trrelind  37957  rp-imass  38065  clsk3nimkb  38338  isotone2  38347  onfrALTlem2  38761  onfrALTlem2VD  39125  unirestss  39307  inmap  39401  fnfvimad  39459  fnfvima2  39478  fsumiunss  39807  islptre  39851  sumnnodd  39862  limclner  39883  liminfval4  40021  liminfval3  40022  cnrefiisplem  40055  cncfuni  40099  ismbl3  40203  ismbl4  40210  fouriersw  40448  qndenserrnbllem  40514  salincl  40543  salgencntex  40561  sge0less  40609  sge0resplit  40623  sge0split  40626  sge0iunmptlemre  40632  carageniuncllem1  40735  carageniuncllem2  40736  caragenel2d  40746  hspmbllem3  40842  hspmbl  40843  ovolval2lem  40857  sssmf  40947  smfaddlem1  40971  smflimlem2  40980  smflimlem3  40981  smflimlem4  40982  smfres  40997  smfmullem4  41001  smfsuplem1  41017  rngcbas  41965  rngchomfval  41966  rngccofval  41970  dfrngc2  41972  rnghmsscmap2  41973  rnghmsscmap  41974  rngcsect  41980  funcrngcsetc  41998  ringcbas  42011  ringchomfval  42012  ringccofval  42016  dfringc2  42018  rhmsscmap2  42019  rhmsscmap  42020  rhmsscrnghm  42026  ringcsect  42031  funcringcsetc  42035  funcringcsetcALTV2lem9  42044  fldc  42083  fldhmsubc  42084  rngcrescrhm  42085  rhmsubclem1  42086  fldcALTV  42101  fldhmsubcALTV  42102  rngcrescrhmALTV  42103  rhmsubcALTVlem1  42104  setrec2fun  42439  setrec2lem1  42440