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

Theorem inss1 3390
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 3359 . . 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 3185 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1685    i^i cin 3152    C_ wss 3153
This theorem is referenced by:  inss2  3391  ssinss1  3398  unabs  3400  nssinpss  3402  dfin4  3410  inv1  3482  disjdif  3527  uniintsn  3900  epse  4375  wefrc  4386  ordtri3or  4423  onfr  4430  ordelinel  4490  relin1  4802  resss  4978  resmpt3  5000  cnvcnvss  5127  funin  5285  funimass2  5292  fnresin1  5324  fnres  5326  fresin  5376  fresaun  5378  fresaunres2  5379  nfvres  5519  ssimaex  5546  fneqeql2  5596  funiunfv  5736  isoini2  5798  ofrfval  6048  ofval  6049  ofrval  6050  off  6055  ofres  6056  ofco  6059  fparlem3  6182  fparlem4  6183  smores  6365  smores2  6367  pmresg  6791  sbthlem7  6973  sbthcl  6979  imafi  7144  ixpfi2  7150  unifpw  7154  f1opwfi  7155  fival  7162  fi0  7169  dffi2  7172  elfiun  7179  dffi3  7180  marypha1lem  7182  ordtypelem3  7231  ordtypelem4  7232  ordtypelem6  7234  ordtypelem7  7235  ordtypelem8  7236  wdomima2g  7296  epfrs  7409  tskwe  7579  r0weon  7636  fodomfi2  7683  infpwfien  7685  ackbij1lem6  7847  ackbij1lem9  7850  ackbij1lem10  7851  ackbij1lem11  7852  ackbij1lem15  7856  ackbij1lem16  7857  fin23lem24  7944  fin23lem26  7947  fin23lem23  7948  fin23lem22  7949  fin23lem19  7958  isfin1-3  8008  ttukeylem6  8137  brdom3  8149  brdom5  8150  brdom4  8151  imadomg  8155  fpwwe2lem12  8259  canthp1lem2  8271  wunin  8331  tskin  8377  gruima  8420  ingru  8433  gruina  8436  grur1a  8437  nqerf  8550  nqerrel  8552  hashun3  11362  hashdif  11371  rexanuz  11825  limsupgle  11947  rlimres  12028  lo1res  12029  lo1resb  12034  rlimresb  12035  o1resb  12036  lo1eq  12038  rlimeq  12039  o1of2  12082  o1rlimmul  12088  isercolllem2  12135  isercolllem3  12136  isercoll  12137  ackbijnn  12282  incexclem  12291  incexc  12292  bitsinvp1  12636  sadcaddlem  12644  sadadd2lem  12646  sadadd3  12648  sadaddlem  12653  sadasslem  12657  sadeq  12659  bitsres  12660  smuval2  12669  smupval  12675  smueqlem  12677  smumul  12680  prmreclem2  12960  ramub2  13057  ramub1lem2  13070  ressinbas  13200  ressress  13201  submre  13503  submrc  13526  isacs2  13551  isacs1i  13555  mreacs  13556  acsfn  13557  invss  13659  sscres  13696  coffth  13806  catcisolem  13934  catciso  13935  catcoppccl  13936  catcfuccl  13937  catcxpccl  13977  isdrs2  14069  isacs3lem  14265  isacs5lem  14268  acsfiindd  14276  psss  14319  psssdm2  14320  tsrss  14328  tsrdir  14356  resscntz  14803  sylow2a  14926  lsmmod  14980  frgpnabllem2  15158  gsumzres  15190  gsumzaddlem  15199  dprddisj2  15270  ablfac1eu  15304  ablfac2  15320  isunit  15435  lspextmo  15809  2idlval  15981  aspsubrg  16067  psrbagsn  16232  mplind  16239  zlpirlem2  16438  pjfval  16602  pjpm  16604  basdif0  16687  tgval2  16690  eltg3  16696  unitg  16701  tgcl  16703  tgdom  16712  tgidm  16714  ppttop  16740  epttop  16742  ntropn  16782  ntrin  16794  mretopd  16825  mreclatdemo  16829  restbas  16885  restfpw  16906  restcls  16907  ordtrest  16928  subbascn  16980  cncls  16999  cnpresti  17012  cnprest  17013  fincmp  17116  cmpsublem  17122  cmpsub  17123  fiuncmp  17127  indiscon  17140  connsub  17143  cnconn  17144  iunconlem  17149  clscon  17152  concompclo  17157  islly2  17206  cldllycmp  17217  kgentopon  17229  llycmpkgen2  17241  1stckgenlem  17244  ptbasfi  17272  txcls  17295  txcnp  17310  ptcnplem  17311  txcnmpt  17314  txcmplem2  17332  hausdiag  17335  txkgen  17342  xkopt  17345  xkococnlem  17349  txcon  17379  qtoptop2  17386  basqtop  17398  tgqtop  17399  kqnrmlem1  17430  kqnrmlem2  17431  nrmhmph  17481  fbssfi  17528  filin  17545  infil  17554  fbasrn  17575  fgtr  17581  ufprim  17600  flimrest  17674  hauspwpwf1  17678  txflf  17697  fclsrest  17715  alexsubALTlem3  17739  alexsubALTlem4  17740  ptcmplem5  17746  tsmsres  17822  tsmsxplem1  17831  xmetres  17924  metres  17925  blin2  17971  blbas  17972  blres  17973  setsmstopn  18020  met2ndci  18064  metrest  18066  ressxms  18067  tgioo  18298  xrsmopn  18314  zdis  18318  reconnlem1  18327  reconnlem2  18328  xrge0tsms  18335  cnheibor  18449  lebnum  18458  nmoleub2lem  18591  nmoleub2lem3  18592  nmoleub2lem2  18593  nmoleub3  18596  nmhmcn  18597  tchcph  18663  cfilresi  18717  cfilres  18718  caussi  18719  causs  18720  relcmpcmet  18738  minveclem4a  18790  minveclem4  18792  ismbl2  18882  cmmbl  18888  nulmbl2  18890  unmbl  18891  shftmbl  18892  volinun  18899  voliunlem1  18903  voliunlem2  18904  ioombl1lem4  18914  ioombl1  18915  ioorcl  18928  uniioombllem2  18934  uniioombllem3  18936  uniioombllem4  18937  uniioombllem5  18938  uniioombl  18940  volivth  18958  vitalilem3  18961  vitalilem4  18962  vitalilem5  18963  vitali  18964  mbfadd  19012  mbfsub  19013  i1fima2  19030  i1fd  19032  i1fadd  19046  itg1addlem2  19048  itg1addlem4  19050  itg1addlem5  19051  itg1climres  19065  mbfmul  19077  itg2splitlem  19099  itg2split  19100  limcresi  19231  limciun  19240  limcun  19241  dvreslem  19255  dvres2lem  19256  dvres  19257  dvres3a  19260  dvaddbr  19283  dvmulbr  19284  dvfsumle  19364  dvfsumabs  19366  ig1peu  19553  taylfvallem1  19732  tayl0  19737  pilem2  19824  pilem3  19825  rlimcnp2  20257  xrlimcnp  20259  ppisval  20337  ppifi  20339  ppiprm  20385  ppinprm  20386  chtprm  20387  chtnprm  20388  chtdif  20392  efchtdvds  20393  ppidif  20397  ppiltx  20411  prmorcht  20412  ppiub  20439  chtlepsi  20441  chtleppi  20445  pclogsum  20450  vmasum  20451  chpval2  20453  chpchtsum  20454  chpub  20455  2sqlem8  20607  chebbnd1lem1  20614  chtppilimlem1  20618  rplogsumlem2  20630  rpvmasum2  20657  dchrisum0re  20658  rplogsum  20672  dirith2  20673  opidon  20983  flddivrng  21076  phnv  21386  minvecolem2  21448  minvecolem3  21449  minvecolem5  21454  minvecolem6  21455  minvecolem7  21456  hlimcaui  21812  chdmm1i  22052  chabs1  22091  chabs2  22092  ledii  22111  lejdii  22113  pjoml4i  22162  cmbr3i  22175  cmbr4i  22176  cmm1i  22181  osumcor2i  22219  3oalem4  22240  pjssmii  22256  pjocini  22273  pjini  22274  mayete3i  22303  mayete3iOLD  22304  riesz4  22640  riesz1  22641  cnlnadjeui  22653  cnlnadjeu  22654  cnlnssadj  22656  nmopadjlei  22664  pjin1i  22768  pjclem1  22771  stji1i  22818  stm1i  22819  dmdbr2  22879  ssmd1  22887  mdslj2i  22896  mdsl2bi  22899  mdslmd1lem1  22901  mdslmd2i  22906  atomli  22958  atcvat4i  22973  sumdmdlem2  22995  dmdbr5ati  22998  dmdbr6ati  22999  dmdbr7ati  23000  infi  23025  ballotlemfelz  23045  ballotlemfp1  23046  conpcon  23173  iccllyscon  23188  cvmsss2  23212  cvmcov2  23213  cvmopnlem  23216  cvmliftmolem2  23220  cvmliftlem15  23236  cvmlift2lem12  23252  nepss  23479  dedekindle  23489  dfon2lem4  23546  predss  23577  wfrlem4  23663  frrlem4  23688  txpss3v  23829  fixssdm  23857  fixssrn  23858  ontopbas  24277  domintrefb  24473  posprsr  24651  dfps2  24700  toplat  24701  reacomsmgrp1  24754  reacomsmgrp2  24755  reacomsmgrp3  24756  reacomsmgrp4  24757  clfsebsr  24760  resgcom  24762  clsint  24924  unint2t  24929  limptlimpr2lem2  24986  flfnei2  24988  islimrs4  24993  stfincomp  25002  lvsovso  25037  hdrmp  25117  inttaror  25311  fneer  25699  fnessref  25704  neibastop1  25719  neibastop2lem  25720  filnetlem3  25740  sstotbnd2  25909  ssbnd  25923  heibor1lem  25944  heiborlem1  25946  heiborlem3  25948  heiborlem5  25950  heiborlem6  25951  heiborlem10  25955  heibor  25956  exidcl  25977  elrfi  26180  elrfirn  26181  elrfirn2  26182  ismrcd1  26184  istopclsd  26186  isnacs2  26192  mrefg3  26194  isnacs3  26196  diophrw  26249  diophin  26263  aomclem2  26563  islmodfg  26578  lsmfgcl  26583  lmhmfgima  26593  lmhmfgsplit  26595  lmhmlnmsplit  26596  frlmsplit2  26654  pwfi2f1o  26671  hbt  26745  acsfn1p  26918  onfrALTlem2  27594  onfrALTlem2VD  27945  bnj1292  28127  lshpinN  28458  lcvexchlem5  28507  pmodlem2  29315  pmod1i  29316  pmodN  29318  osumcllem7N  29430  pexmidlem4N  29441  pl42lem3N  29449  djaclN  30605  dihoml4c  30845  dochdmj1  30859  djhcl  30869  dochexmidlem4  30932  mapd1o  31117  mapdin  31131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator