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

Theorem inss1 3402
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 3371 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 446 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3197 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1696    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  inss2  3403  ssinss1  3410  unabs  3412  nssinpss  3414  dfin4  3422  inv1  3494  disjdif  3539  uniintsn  3915  epse  4392  wefrc  4403  ordtri3or  4440  onfr  4447  ordelinel  4507  relin1  4819  resss  4995  resmpt3  5017  cnvcnvss  5144  funin  5335  funimass2  5342  fnresin1  5374  fnres  5376  fresin  5426  fresaun  5428  fresaunres2  5429  nfvres  5573  ssimaex  5600  fneqeql2  5650  funiunfv  5790  isoini2  5852  ofrfval  6102  ofval  6103  ofrval  6104  off  6109  ofres  6110  ofco  6113  fparlem3  6236  fparlem4  6237  smores  6385  smores2  6387  pmresg  6811  sbthlem7  6993  sbthcl  6999  imafi  7164  ixpfi2  7170  unifpw  7174  f1opwfi  7175  fival  7182  fi0  7189  dffi2  7192  elfiun  7199  dffi3  7200  marypha1lem  7202  ordtypelem3  7251  ordtypelem4  7252  ordtypelem6  7254  ordtypelem7  7255  ordtypelem8  7256  wdomima2g  7316  epfrs  7429  tskwe  7599  r0weon  7656  fodomfi2  7703  infpwfien  7705  ackbij1lem6  7867  ackbij1lem9  7870  ackbij1lem10  7871  ackbij1lem11  7872  ackbij1lem15  7876  ackbij1lem16  7877  fin23lem24  7964  fin23lem26  7967  fin23lem23  7968  fin23lem22  7969  fin23lem19  7978  isfin1-3  8028  ttukeylem6  8157  brdom3  8169  brdom5  8170  brdom4  8171  imadomg  8175  fpwwe2lem12  8279  canthp1lem2  8291  wunin  8351  tskin  8397  gruima  8440  ingru  8453  gruina  8456  grur1a  8457  nqerf  8570  nqerrel  8572  hashun3  11382  hashdif  11391  rexanuz  11845  limsupgle  11967  rlimres  12048  lo1res  12049  lo1resb  12054  rlimresb  12055  o1resb  12056  lo1eq  12058  rlimeq  12059  o1of2  12102  o1rlimmul  12108  isercolllem2  12155  isercolllem3  12156  isercoll  12157  ackbijnn  12302  incexclem  12311  incexc  12312  bitsinvp1  12656  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  sadaddlem  12673  sadasslem  12677  sadeq  12679  bitsres  12680  smuval2  12689  smupval  12695  smueqlem  12697  smumul  12700  prmreclem2  12980  ramub2  13077  ramub1lem2  13090  ressinbas  13220  ressress  13221  submre  13523  submrc  13546  isacs2  13571  isacs1i  13575  mreacs  13576  acsfn  13577  invss  13679  sscres  13716  coffth  13826  catcisolem  13954  catciso  13955  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997  isdrs2  14089  isacs3lem  14285  isacs5lem  14288  acsfiindd  14296  psss  14339  psssdm2  14340  tsrss  14348  tsrdir  14376  resscntz  14823  sylow2a  14946  lsmmod  15000  frgpnabllem2  15178  gsumzres  15210  gsumzaddlem  15219  dprddisj2  15290  ablfac1eu  15324  ablfac2  15340  isunit  15455  lspextmo  15829  2idlval  16001  aspsubrg  16087  psrbagsn  16252  mplind  16259  zlpirlem2  16458  pjfval  16622  pjpm  16624  basdif0  16707  tgval2  16710  eltg3  16716  unitg  16721  tgcl  16723  tgdom  16732  tgidm  16734  ppttop  16760  epttop  16762  ntropn  16802  ntrin  16814  mretopd  16845  mreclatdemo  16849  restbas  16905  restfpw  16926  restcls  16927  ordtrest  16948  subbascn  17000  cncls  17019  cnpresti  17032  cnprest  17033  fincmp  17136  cmpsublem  17142  cmpsub  17143  fiuncmp  17147  indiscon  17160  connsub  17163  cnconn  17164  iunconlem  17169  clscon  17172  concompclo  17177  islly2  17226  cldllycmp  17237  kgentopon  17249  llycmpkgen2  17261  1stckgenlem  17264  ptbasfi  17292  txcls  17315  txcnp  17330  ptcnplem  17331  txcnmpt  17334  txcmplem2  17352  hausdiag  17355  txkgen  17362  xkopt  17365  xkococnlem  17369  txcon  17399  qtoptop2  17406  basqtop  17418  tgqtop  17419  kqnrmlem1  17450  kqnrmlem2  17451  nrmhmph  17501  fbssfi  17548  filin  17565  infil  17574  fbasrn  17595  fgtr  17601  ufprim  17620  flimrest  17694  hauspwpwf1  17698  txflf  17717  fclsrest  17735  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem5  17766  tsmsres  17842  tsmsxplem1  17851  xmetres  17944  metres  17945  blin2  17991  blbas  17992  blres  17993  setsmstopn  18040  met2ndci  18084  metrest  18086  ressxms  18087  tgioo  18318  xrsmopn  18334  zdis  18338  reconnlem1  18347  reconnlem2  18348  xrge0tsms  18355  cnheibor  18469  lebnum  18478  nmoleub2lem  18611  nmoleub2lem3  18612  nmoleub2lem2  18613  nmoleub3  18616  nmhmcn  18617  tchcph  18683  cfilresi  18737  cfilres  18738  caussi  18739  causs  18740  relcmpcmet  18758  minveclem4a  18810  minveclem4  18812  ismbl2  18902  cmmbl  18908  nulmbl2  18910  unmbl  18911  shftmbl  18912  volinun  18919  voliunlem1  18923  voliunlem2  18924  ioombl1lem4  18934  ioombl1  18935  ioorcl  18948  uniioombllem2  18954  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombl  18960  volivth  18978  vitalilem3  18981  vitalilem4  18982  vitalilem5  18983  vitali  18984  mbfadd  19032  mbfsub  19033  i1fima2  19050  i1fd  19052  i1fadd  19066  itg1addlem2  19068  itg1addlem4  19070  itg1addlem5  19071  itg1climres  19085  mbfmul  19097  itg2splitlem  19119  itg2split  19120  limcresi  19251  limciun  19260  limcun  19261  dvreslem  19275  dvres2lem  19276  dvres  19277  dvres3a  19280  dvaddbr  19303  dvmulbr  19304  dvfsumle  19384  dvfsumabs  19386  ig1peu  19573  taylfvallem1  19752  tayl0  19757  pilem2  19844  pilem3  19845  rlimcnp2  20277  xrlimcnp  20279  ppisval  20357  ppifi  20359  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  chtdif  20412  efchtdvds  20413  ppidif  20417  ppiltx  20431  prmorcht  20432  ppiub  20459  chtlepsi  20461  chtleppi  20465  pclogsum  20470  vmasum  20471  chpval2  20473  chpchtsum  20474  chpub  20475  2sqlem8  20627  chebbnd1lem1  20634  chtppilimlem1  20638  rplogsumlem2  20650  rpvmasum2  20677  dchrisum0re  20678  rplogsum  20692  dirith2  20693  opidon  21005  flddivrng  21098  phnv  21408  minvecolem2  21470  minvecolem3  21471  minvecolem5  21476  minvecolem6  21477  minvecolem7  21478  hlimcaui  21832  chdmm1i  22072  chabs1  22111  chabs2  22112  ledii  22131  lejdii  22133  pjoml4i  22182  cmbr3i  22195  cmbr4i  22196  cmm1i  22201  osumcor2i  22239  3oalem4  22260  pjssmii  22276  pjocini  22293  pjini  22294  mayete3i  22323  mayete3iOLD  22324  riesz4  22660  riesz1  22661  cnlnadjeui  22673  cnlnadjeu  22674  cnlnssadj  22676  nmopadjlei  22684  pjin1i  22788  pjclem1  22791  stji1i  22838  stm1i  22839  dmdbr2  22899  ssmd1  22907  mdslj2i  22916  mdsl2bi  22919  mdslmd1lem1  22921  mdslmd2i  22926  atomli  22978  atcvat4i  22993  sumdmdlem2  23015  dmdbr5ati  23018  dmdbr6ati  23019  dmdbr7ati  23020  infi  23045  ballotlemfelz  23065  ballotlemfp1  23066  infi1  23185  off2  23223  disjin  23377  xrge0tsmsd  23397  esumval  23440  esumel  23441  esumcst  23451  esumpcvgval  23461  esumcvg  23469  sigainb  23512  measinb2  23565  indf1ofs  23624  conpcon  23781  iccllyscon  23796  cvmsss2  23820  cvmcov2  23821  cvmopnlem  23824  cvmliftmolem2  23828  cvmliftlem15  23844  cvmlift2lem12  23860  nepss  24087  dedekindle  24098  dfon2lem4  24213  predss  24244  wfrlem4  24330  frrlem4  24355  nofulllem5  24431  txpss3v  24489  fixssdm  24517  fixssrn  24518  ontopbas  24939  domintrefb  25166  posprsr  25343  dfps2  25392  toplat  25393  reacomsmgrp1  25446  reacomsmgrp2  25447  reacomsmgrp3  25448  reacomsmgrp4  25449  clfsebsr  25452  resgcom  25454  clsint  25616  unint2t  25621  limptlimpr2lem2  25678  flfnei2  25680  islimrs4  25685  stfincomp  25694  lvsovso  25729  hdrmp  25809  inttaror  26003  fneer  26391  fnessref  26396  neibastop1  26411  neibastop2lem  26412  filnetlem3  26432  sstotbnd2  26601  ssbnd  26615  heibor1lem  26636  heiborlem1  26638  heiborlem3  26640  heiborlem5  26642  heiborlem6  26643  heiborlem10  26647  heibor  26648  exidcl  26669  elrfi  26872  elrfirn  26873  elrfirn2  26874  ismrcd1  26876  istopclsd  26878  isnacs2  26884  mrefg3  26886  isnacs3  26888  diophrw  26941  diophin  26955  aomclem2  27255  islmodfg  27270  lsmfgcl  27275  lmhmfgima  27285  lmhmfgsplit  27287  lmhmlnmsplit  27288  frlmsplit2  27346  pwfi2f1o  27363  hbt  27437  acsfn1p  27610  onfrALTlem2  28610  onfrALTlem2VD  28981  bnj1292  29164  lshpinN  29801  lcvexchlem5  29850  pmodlem2  30658  pmod1i  30659  pmodN  30661  osumcllem7N  30773  pexmidlem4N  30784  pl42lem3N  30792  djaclN  31948  dihoml4c  32188  dochdmj1  32202  djhcl  32212  dochexmidlem4  32275  mapd1o  32460  mapdin  32474
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator