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

Theorem inss1 3673
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  |-  ( A  i^i  B )  C_  A

Proof of Theorem inss1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elin 3642 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 460 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3463 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758    i^i cin 3430    C_ wss 3431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-v 3074  df-in 3438  df-ss 3445
This theorem is referenced by:  inss2  3674  ssinss1  3681  unabs  3683  nssinpss  3685  dfin4  3693  inv1  3767  disjdif  3854  uniintsn  4268  wefrc  4817  ordtri3or  4854  onfr  4861  ordelinel  4920  relin1  5060  resss  5237  resmpt3  5260  cnvcnvss  5395  funin  5588  funimass2  5595  fnresin1  5628  fnres  5630  fresin  5683  fresaun  5685  fresaunres2  5686  nfvres  5824  ssimaex  5860  fneqeql2  5916  funiunfv  6069  isoini2  6134  ofrfval  6433  ofval  6434  ofrval  6435  off  6439  ofres  6440  ofco  6445  fparlem3  6779  fparlem4  6780  smores  6918  smores2  6920  tfrlem5  6944  pmresg  7345  sbthlem7  7532  sbthcl  7538  infi  7642  imafi  7710  ixpfi2  7715  unifpw  7720  f1opwfi  7721  fival  7768  fi0  7776  dffi2  7779  elfiun  7786  dffi3  7787  marypha1lem  7789  ordtypelem3  7840  ordtypelem4  7841  ordtypelem6  7843  ordtypelem7  7844  ordtypelem8  7845  wdomima2g  7907  epfrs  8057  tskwe  8226  r0weon  8285  fodomfi2  8336  infpwfien  8338  ackbij1lem6  8500  ackbij1lem9  8503  ackbij1lem10  8504  ackbij1lem11  8505  ackbij1lem15  8509  ackbij1lem16  8510  fin23lem24  8597  fin23lem26  8600  fin23lem23  8601  fin23lem22  8602  fin23lem19  8611  isfin1-3  8661  ttukeylem6  8789  brdom3  8801  brdom5  8802  brdom4  8803  imadomg  8807  fpwwe2lem12  8914  canthp1lem2  8926  wunin  8986  tskin  9032  gruima  9075  ingru  9088  gruina  9091  grur1a  9092  nqerf  9205  nqerrel  9207  dedekindle  9640  hashun3  12260  hashdif  12281  rexanuz  12946  limsupgle  13068  rlimres  13149  lo1res  13150  lo1resb  13155  rlimresb  13156  o1resb  13157  lo1eq  13159  rlimeq  13160  o1of2  13203  o1rlimmul  13209  isercolllem2  13256  isercolllem3  13257  isercoll  13258  ackbijnn  13404  incexclem  13412  incexc  13413  bitsinvp1  13758  sadcaddlem  13766  sadadd2lem  13768  sadadd3  13770  sadaddlem  13775  sadasslem  13779  sadeq  13781  bitsres  13782  smuval2  13791  smupval  13797  smueqlem  13799  smumul  13802  prmreclem2  14091  ramub2  14188  ramub1lem2  14201  fvsetsid  14312  ressinbas  14348  ressress  14349  submre  14657  submrc  14680  isacs2  14705  isacs1i  14709  mreacs  14710  acsfn  14711  invss  14813  sscres  14850  coffth  14960  catcisolem  15088  catciso  15089  catcoppccl  15090  catcfuccl  15091  catcxpccl  15131  isdrs2  15223  isacs3lem  15450  isacs5lem  15453  acsfiindd  15461  psss  15498  psssdm2  15499  tsrss  15507  tsrdir  15522  resscntz  15963  sylow2a  16234  lsmmod  16288  frgpnabllem2  16468  gsumzres  16504  gsumzresOLD  16508  gsumzaddlem  16524  gsumzaddlemOLD  16526  dprddisj2  16654  dprddisj2OLD  16655  ablfac1eu  16691  ablfac2  16707  isunit  16867  lspextmo  17255  2idlval  17433  aspsubrg  17520  psrbagsn  17696  mplind  17703  zringlpirlem2  18024  zlpirlem2  18029  pjfval  18251  pjpm  18253  ofco2  18454  basdif0  18685  tgval2  18688  eltg3  18694  unitg  18699  tgcl  18701  tgdom  18710  tgidm  18712  ppttop  18738  epttop  18740  ntropn  18780  ntrin  18792  mretopd  18823  mreclatdemoBAD  18827  neiptoptop  18862  restbas  18889  restfpw  18910  neitr  18911  restcls  18912  ordtrest  18933  subbascn  18985  cncls  19005  cnpresti  19019  cnprest  19020  fincmp  19123  cmpsublem  19129  cmpsub  19130  fiuncmp  19134  indiscon  19149  connsub  19152  cnconn  19153  iunconlem  19158  clscon  19161  concompclo  19166  islly2  19215  cldllycmp  19226  kgentopon  19238  llycmpkgen2  19250  1stckgenlem  19253  ptbasfi  19281  txcls  19304  txcnp  19320  ptcnplem  19321  txcnmpt  19324  txcmplem2  19342  hausdiag  19345  txkgen  19352  xkopt  19355  xkococnlem  19359  txcon  19389  qtoptop2  19399  basqtop  19411  tgqtop  19412  kqnrmlem1  19443  kqnrmlem2  19444  nrmhmph  19494  fbssfi  19537  filin  19554  infil  19563  fbasrn  19584  fgtr  19590  ufprim  19609  flimrest  19683  hauspwpwf1  19687  txflf  19706  fclsrest  19724  alexsubALTlem3  19748  alexsubALTlem4  19749  ptcmplem5  19755  tsmsresOLD  19844  tsmsres  19845  tsmsxplem1  19854  ustund  19923  trust  19931  utoptop  19936  restutop  19939  cfiluweak  19997  xmetres  20066  metres  20067  blin2  20131  blbas  20132  blres  20133  setsmstopn  20180  met2ndci  20224  metrest  20226  ressxms  20227  tgioo  20500  xrsmopn  20516  zdis  20520  reconnlem1  20530  reconnlem2  20531  xrge0tsms  20538  cnheibor  20654  lebnum  20663  nmoleub2lem  20796  nmoleub2lem3  20797  nmoleub2lem2  20798  nmoleub3  20801  nmhmcn  20802  tchcph  20879  cfilresi  20933  cfilres  20934  caussi  20935  causs  20936  relcmpcmet  20954  minveclem4a  21044  minveclem4  21046  ismbl2  21137  cmmbl  21144  nulmbl2  21146  unmbl  21147  shftmbl  21148  volinun  21155  voliunlem1  21159  voliunlem2  21160  ioombl1lem4  21170  ioombl1  21171  ioorcl  21185  uniioombllem2  21191  uniioombllem3  21193  uniioombllem4  21194  uniioombllem5  21195  uniioombl  21197  volivth  21215  vitalilem3  21218  vitalilem4  21219  vitalilem5  21220  vitali  21221  mbfadd  21267  mbfsub  21268  i1fima2  21285  i1fd  21287  i1fadd  21301  itg1addlem2  21303  itg1addlem4  21305  itg1addlem5  21306  itg1climres  21320  mbfmul  21332  itg2splitlem  21354  itg2split  21355  limcresi  21488  limciun  21497  limcun  21498  dvreslem  21512  dvres2lem  21513  dvres  21514  dvres3a  21517  dvaddbr  21540  dvmulbr  21541  dvfsumle  21621  dvfsumabs  21623  ig1peu  21771  taylfvallem1  21950  tayl0  21955  pilem2  22045  pilem3  22046  rlimcnp2  22488  xrlimcnp  22490  ppisval  22569  ppifi  22571  ppiprm  22617  ppinprm  22618  chtprm  22619  chtnprm  22620  chtdif  22624  efchtdvds  22625  ppidif  22629  ppiltx  22643  prmorcht  22644  ppiub  22671  chtlepsi  22673  chtleppi  22677  pclogsum  22682  vmasum  22683  chpval2  22685  chpchtsum  22686  chpub  22687  2sqlem8  22839  chebbnd1lem1  22846  chtppilimlem1  22850  rplogsumlem2  22862  rpvmasum2  22889  dchrisum0re  22890  rplogsum  22904  dirith2  22905  axtgcgrrflx  23051  axtgcgrid  23052  axtgsegcon  23053  axtg5seg  23054  axtgbtwnid  23055  axtgpasch  23056  axtgcont1  23057  perpcom  23244  perpneq  23245  ragperp  23248  opidon  23956  flddivrng  24049  phnv  24361  minvecolem2  24423  minvecolem3  24424  minvecolem5  24429  minvecolem6  24430  minvecolem7  24431  hlimcaui  24786  chdmm1i  25027  chabs1  25066  chabs2  25067  ledii  25086  lejdii  25088  pjoml4i  25137  cmbr3i  25150  cmbr4i  25151  cmm1i  25156  osumcor2i  25194  3oalem4  25215  pjssmii  25231  pjocini  25248  pjini  25249  mayete3i  25278  mayete3iOLD  25279  riesz4  25615  riesz1  25616  cnlnadjeui  25628  cnlnadjeu  25629  cnlnssadj  25631  nmopadjlei  25639  pjin1i  25743  pjclem1  25746  stji1i  25793  stm1i  25794  dmdbr2  25854  ssmd1  25862  mdslj2i  25871  mdsl2bi  25874  mdslmd1lem1  25876  mdslmd2i  25881  atomli  25933  atcvat4i  25948  sumdmdlem2  25970  dmdbr5ati  25973  dmdbr6ati  25974  dmdbr7ati  25975  disjin  26075  disjxpin  26076  imadifxp  26085  off2  26105  ffsrn  26175  gsumle  26386  xrge0tsmsd  26393  ordtrestNEW  26491  qqhnm  26559  qqhcn  26560  rrhre  26587  indf1ofs  26622  esumval  26640  esumel  26641  gsumesum  26650  esumlub  26651  esumcst  26654  esumfsup  26659  esumpcvgval  26667  esumcvg  26675  sigainb  26719  measunl  26770  measinb2  26777  sibfinima  26864  sibfof  26865  eulerpartlemelr  26879  eulerpartlem1  26889  eulerpartgbij  26894  eulerpartlemgvv  26898  eulerpartlemgu  26899  eulerpartlemgs2  26902  sseqf  26914  ballotlemfelz  27012  ballotlemfp1  27013  conpcon  27263  iccllyscon  27278  cvmsss2  27302  cvmcov2  27303  cvmopnlem  27306  cvmliftmolem2  27310  cvmliftlem15  27326  cvmlift2lem12  27342  nepss  27513  dfon2lem4  27738  predss  27771  wfrlem4  27866  frrlem4  27910  nofulllem5  27986  txpss3v  28048  fixssdm  28076  fixssrn  28077  limitssson  28081  ontopbas  28413  ptrest  28568  mblfinlem3  28573  mblfinlem4  28574  ismblfin  28575  mbfposadd  28582  fneer  28703  fnessref  28708  neibastop1  28723  neibastop2lem  28724  filnetlem3  28744  sstotbnd2  28816  ssbnd  28830  heibor1lem  28851  heiborlem1  28853  heiborlem3  28855  heiborlem5  28857  heiborlem6  28858  heiborlem10  28862  heibor  28863  exidcl  28884  elrfi  29173  elrfirn  29174  elrfirn2  29175  ismrcd1  29177  istopclsd  29179  isnacs2  29185  mrefg3  29187  isnacs3  29189  diophrw  29240  diophin  29254  aomclem2  29551  islmodfg  29565  lsmfgcl  29570  lmhmfgima  29580  lmhmfgsplit  29582  lmhmlnmsplit  29583  pwfi2f1o  29594  hbt  29629  acsfn1p  29699  onfrALTlem2  31567  onfrALTlem2VD  31938  bnj1292  32122  bj-ablssgrp  32893  lshpinN  32953  lcvexchlem5  33002  pmodlem2  33810  pmod1i  33811  pmodN  33813  osumcllem7N  33925  pexmidlem4N  33936  pl42lem3N  33944  djaclN  35100  dihoml4c  35340  dochdmj1  35354  djhcl  35364  dochexmidlem4  35427  mapd1o  35612  mapdin  35626  taupilemrplb  35933  taupilem2  35935  taupi  35936
  Copyright terms: Public domain W3C validator