MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inss1 Structured version   Visualization version   GIF version

Theorem inss1 3795
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.
StepHypRef Expression
1 elinel1 3761 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3572 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cin 3539  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554
This theorem is referenced by:  inss2  3796  ssinss1  3803  unabs  3816  nssinpss  3818  dfin4  3826  inv1  3922  disjdif  3992  uniintsn  4449  wefrc  5032  relin1  5159  resss  5342  resmpt3  5370  cnvcnvss  5507  predss  5604  ordtri3or  5672  onfr  5680  ordelinel  5742  ordelinelOLD  5743  funin  5879  funimass2  5886  fnresin1  5919  fnres  5921  fresin  5986  fresaun  5988  fresaunres2  5989  nfvres  6134  ssimaex  6173  fneqeql2  6234  funiunfv  6410  isoini2  6489  ofrfval  6803  ofval  6804  ofrval  6805  off  6810  ofres  6811  ofco  6815  fparlem3  7166  fparlem4  7167  wfrlem4  7305  smores  7336  smores2  7338  tfrlem5  7363  pmresg  7771  sbthlem7  7961  sbthcl  7967  infi  8069  imafi  8142  ixpfi2  8147  unifpw  8152  f1opwfi  8153  fival  8201  fi0  8209  dffi2  8212  elfiun  8219  dffi3  8220  marypha1lem  8222  ordtypelem3  8308  ordtypelem4  8309  ordtypelem6  8311  ordtypelem7  8312  ordtypelem8  8313  wdomima2g  8374  epfrs  8490  tskwe  8659  r0weon  8718  fodomfi2  8766  infpwfien  8768  ackbij1lem6  8930  ackbij1lem9  8933  ackbij1lem10  8934  ackbij1lem11  8935  ackbij1lem15  8939  ackbij1lem16  8940  fin23lem24  9027  fin23lem26  9030  fin23lem23  9031  fin23lem22  9032  fin23lem19  9041  isfin1-3  9091  ttukeylem6  9219  brdom3  9231  brdom5  9232  brdom4  9233  imadomg  9237  fpwwe2lem12  9342  canthp1lem2  9354  wunin  9414  tskin  9460  gruima  9503  ingru  9516  gruina  9519  grur1a  9520  nqerf  9631  nqerrel  9633  dedekindle  10080  hashun3  13034  hashin  13060  hashdif  13062  xptrrel  13567  rexanuz  13933  limsupgle  14056  rlimres  14137  lo1res  14138  lo1resb  14143  rlimresb  14144  o1resb  14145  lo1eq  14147  rlimeq  14148  o1of2  14191  o1rlimmul  14197  isercolllem2  14244  isercolllem3  14245  isercoll  14246  ackbijnn  14399  incexclem  14407  incexc  14408  bitsinvp1  15009  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  sadasslem  15030  sadeq  15032  bitsres  15033  smuval2  15042  smupval  15048  smueqlem  15050  smumul  15053  ramub2  15556  ramub1lem2  15569  fvsetsid  15722  ressinbas  15763  ressress  15765  submre  16088  submrc  16111  isacs2  16137  isacs1i  16141  mreacs  16142  acsfn  16143  invss  16244  sscres  16306  coffth  16419  catcisolem  16579  catciso  16580  catcoppccl  16581  catcfuccl  16582  catcxpccl  16670  isdrs2  16762  isacs3lem  16989  isacs5lem  16992  acsfiindd  17000  psss  17037  psssdm2  17038  tsrss  17046  tsrdir  17061  resscntz  17587  sylow2a  17857  lsmmod  17911  frgpnabllem2  18100  gsumzres  18133  gsumzaddlem  18144  dprddisj2  18261  ablfac1eu  18295  ablfac2  18311  isunit  18480  lspextmo  18877  2idlval  19054  aspsubrg  19152  psrbagsn  19316  mplind  19323  zringlpirlem2  19652  pjfval  19869  pjpm  19871  ofco2  20076  basdif0  20568  tgval2  20571  eltg3  20577  tgcl  20584  tgdom  20593  tgidm  20595  ppttop  20621  epttop  20623  ntropn  20663  ntrin  20675  mretopd  20706  mreclatdemoBAD  20710  neiptoptop  20745  restbas  20772  restfpw  20793  neitr  20794  restcls  20795  ordtrest  20816  subbascn  20868  cncls  20888  cnpresti  20902  cnprest  20903  fincmp  21006  cmpsublem  21012  cmpsub  21013  fiuncmp  21017  indiscon  21031  connsub  21034  cnconn  21035  iunconlem  21040  clscon  21043  concompclo  21048  islly2  21097  cldllycmp  21108  kgentopon  21151  llycmpkgen2  21163  1stckgenlem  21166  ptbasfi  21194  txcls  21217  txcnp  21233  ptcnplem  21234  txcnmpt  21237  txcmplem2  21255  hausdiag  21258  txkgen  21265  xkopt  21268  xkococnlem  21272  txcon  21302  qtoptop2  21312  basqtop  21324  tgqtop  21325  kqnrmlem1  21356  kqnrmlem2  21357  nrmhmph  21407  fbssfi  21451  filin  21468  infil  21477  fbasrn  21498  fgtr  21504  ufprim  21523  flimrest  21597  hauspwpwf1  21601  txflf  21620  fclsrest  21638  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem5  21670  tsmsres  21757  tsmsxplem1  21766  ustund  21835  trust  21843  utoptop  21848  restutop  21851  cfiluweak  21909  xmetres  21979  metres  21980  blin2  22044  blbas  22045  blres  22046  setsmstopn  22093  met2ndci  22137  metrest  22139  ressxms  22140  tgioo  22407  xrsmopn  22423  zdis  22427  reconnlem1  22437  reconnlem2  22438  xrge0tsms  22445  cnheibor  22562  lebnum  22571  nmoleub2lem  22722  nmoleub2lem2  22724  nmhmcn  22728  tchcph  22844  cfilresi  22901  cfilres  22902  caussi  22903  causs  22904  relcmpcmet  22923  minveclem4a  23009  minveclem4  23011  ismbl2  23102  cmmbl  23109  nulmbl2  23111  unmbl  23112  shftmbl  23113  volinun  23121  voliunlem1  23125  voliunlem2  23126  ioombl1lem4  23136  ioombl1  23137  ioorcl  23151  uniioombllem2  23157  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombl  23163  volivth  23181  vitalilem3  23185  vitalilem4  23186  vitalilem5  23187  vitali  23188  mbfadd  23234  mbfsub  23235  i1fima2  23252  i1fd  23254  i1fadd  23268  itg1addlem2  23270  itg1addlem4  23272  itg1addlem5  23273  itg1climres  23287  mbfmul  23299  itg2splitlem  23321  itg2split  23322  limcresi  23455  limciun  23464  limcun  23465  dvreslem  23479  dvres2lem  23480  dvres  23481  dvres3a  23484  dvaddbr  23507  dvmulbr  23508  dvfsumle  23588  dvfsumabs  23590  ig1peu  23735  taylfvallem1  23915  pilem2  24010  pilem3  24011  rlimcnp2  24493  xrlimcnp  24495  ppisval  24630  ppifi  24632  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  chtdif  24684  efchtdvds  24685  ppidif  24689  ppiltx  24703  prmorcht  24704  ppiub  24729  chtlepsi  24731  chtleppi  24735  pclogsum  24740  vmasum  24741  chpval2  24743  chpchtsum  24744  chpub  24745  2sqlem8  24951  chebbnd1lem1  24958  chtppilimlem1  24962  rplogsumlem2  24974  rpvmasum2  25001  dchrisum0re  25002  rplogsum  25016  dirith2  25017  axtgcgrrflx  25161  axtgcgrid  25162  axtgsegcon  25163  axtg5seg  25164  axtgbtwnid  25165  axtgpasch  25166  axtgcont1  25167  perpcom  25408  perpneq  25409  ragperp  25412  phnv  27053  minvecolem2  27115  minvecolem3  27116  minvecolem5  27121  minvecolem6  27122  minvecolem7  27123  hlimcaui  27477  chdmm1i  27720  chabs1  27759  chabs2  27760  ledii  27779  lejdii  27781  pjoml4i  27830  cmbr3i  27843  cmbr4i  27844  cmm1i  27849  osumcor2i  27887  3oalem4  27908  pjssmii  27924  pjocini  27941  pjini  27942  mayete3i  27971  riesz4  28307  riesz1  28308  cnlnadjeui  28320  cnlnadjeu  28321  cnlnssadj  28323  nmopadjlei  28331  pjin1i  28435  pjclem1  28438  stji1i  28485  stm1i  28486  dmdbr2  28546  ssmd1  28554  mdslj2i  28563  mdsl2bi  28566  mdslmd1lem1  28568  mdslmd2i  28573  atomli  28625  atcvat4i  28640  sumdmdlem2  28662  dmdbr5ati  28665  dmdbr6ati  28666  dmdbr7ati  28667  disjin  28781  disjxpin  28783  imadifxp  28796  off2  28823  ffsrn  28892  gsummptres  29115  xrge0tsmsd  29116  ordtrestNEW  29295  qqhnm  29362  qqhcn  29363  rrhre  29393  indf1ofs  29415  esumval  29435  esumel  29436  gsumesum  29448  esumlub  29449  esumcst  29452  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  sigainb  29526  ldgenpisyslem1  29553  measinb2  29613  sibfinima  29728  sibfof  29729  eulerpartlemelr  29746  eulerpartlem1  29756  eulerpartgbij  29761  eulerpartlemgvv  29765  eulerpartlemgu  29766  eulerpartlemgs2  29769  sseqf  29781  ballotlemfelz  29879  ballotlemfp1  29880  bnj1292  30140  conpcon  30471  iccllyscon  30486  cvmsss2  30510  cvmcov2  30511  cvmopnlem  30514  cvmliftmolem2  30518  cvmliftlem15  30534  cvmlift2lem12  30550  mvrsfpw  30657  msrf  30693  elmsta  30699  mthmpps  30733  nepss  30854  dfon2lem4  30935  frrlem4  31027  nofulllem5  31105  txpss3v  31155  fixssdm  31183  fixssrn  31184  limitssson  31188  fneer  31518  neibastop1  31524  neibastop2lem  31525  filnetlem3  31545  ontopbas  31597  bj-restpw  32226  bj-ablssgrp  32315  taupilemrplb  32343  taupilem2  32345  taupi  32346  ptrest  32578  poimirlem29  32608  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  mbfposadd  32627  sstotbnd2  32743  ssbnd  32757  heibor1lem  32778  heiborlem1  32780  heiborlem3  32782  heiborlem5  32784  heiborlem6  32785  heiborlem10  32789  heibor  32790  opidonOLD  32821  exidcl  32845  flddivrng  32968  lshpinN  33294  lcvexchlem5  33343  pmodlem2  34151  pmod1i  34152  pmodN  34154  osumcllem7N  34266  pexmidlem4N  34277  pl42lem3N  34285  djaclN  35443  dihoml4c  35683  dochdmj1  35697  djhcl  35707  dochexmidlem4  35770  mapd1o  35955  mapdin  35969  elrfi  36275  elrfirn  36276  elrfirn2  36277  ismrcd1  36279  istopclsd  36281  isnacs2  36287  mrefg3  36289  isnacs3  36291  diophrw  36340  diophin  36354  aomclem2  36643  islmodfg  36657  lsmfgcl  36662  lmhmfgima  36672  lmhmfgsplit  36674  lmhmlnmsplit  36675  pwfi2f1o  36684  hbt  36719  acsfn1p  36788  elinintrab  36902  trrelind  36976  rp-imass  37085  clsk3nimkb  37358  isotone2  37367  onfrALTlem2  37782  onfrALTlem2VD  38147  unirestss  38339  inmap  38396  fsumiunss  38642  islptre  38686  sumnnodd  38697  limclner  38718  cncfuni  38772  ismbl3  38879  ismbl4  38886  fouriersw  39124  qndenserrnbllem  39190  salincl  39219  salgencntex  39237  sge0less  39285  sge0resplit  39299  sge0split  39302  sge0iunmptlemre  39308  carageniuncllem1  39411  carageniuncllem2  39412  caragenel2d  39422  hspmbllem3  39518  hspmbl  39519  ovolval2lem  39533  sssmf  39625  smfaddlem1  39649  smflimlem2  39658  smflimlem3  39659  smflimlem4  39660  smfres  39675  smfmullem4  39679  rngcbas  41757  rngchomfval  41758  rngccofval  41762  dfrngc2  41764  rnghmsscmap2  41765  rnghmsscmap  41766  rngcsect  41772  funcrngcsetc  41790  ringcbas  41803  ringchomfval  41804  ringccofval  41808  dfringc2  41810  rhmsscmap2  41811  rhmsscmap  41812  rhmsscrnghm  41818  ringcsect  41823  funcringcsetc  41827  funcringcsetcALTV2lem9  41836  fldc  41875  fldhmsubc  41876  rngcrescrhm  41877  rhmsubclem1  41878  fldcALTV  41894  fldhmsubcALTV  41895  rngcrescrhmALTV  41896  rhmsubcALTVlem1  41897  setrec2fun  42238  setrec2lem1  42239
  Copyright terms: Public domain W3C validator