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

Theorem inss1 3391
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 3360 . . 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 3186 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1686    i^i cin 3153    C_ wss 3154
This theorem is referenced by:  inss2  3392  ssinss1  3399  unabs  3401  nssinpss  3403  dfin4  3411  inv1  3483  disjdif  3528  uniintsn  3901  epse  4378  wefrc  4389  ordtri3or  4426  onfr  4433  ordelinel  4493  relin1  4805  resss  4981  resmpt3  5003  cnvcnvss  5130  funin  5321  funimass2  5328  fnresin1  5360  fnres  5362  fresin  5412  fresaun  5414  fresaunres2  5415  nfvres  5559  ssimaex  5586  fneqeql2  5636  funiunfv  5776  isoini2  5838  ofrfval  6088  ofval  6089  ofrval  6090  off  6095  ofres  6096  ofco  6099  fparlem3  6222  fparlem4  6223  smores  6371  smores2  6373  pmresg  6797  sbthlem7  6979  sbthcl  6985  imafi  7150  ixpfi2  7156  unifpw  7160  f1opwfi  7161  fival  7168  fi0  7175  dffi2  7178  elfiun  7185  dffi3  7186  marypha1lem  7188  ordtypelem3  7237  ordtypelem4  7238  ordtypelem6  7240  ordtypelem7  7241  ordtypelem8  7242  wdomima2g  7302  epfrs  7415  tskwe  7585  r0weon  7642  fodomfi2  7689  infpwfien  7691  ackbij1lem6  7853  ackbij1lem9  7856  ackbij1lem10  7857  ackbij1lem11  7858  ackbij1lem15  7862  ackbij1lem16  7863  fin23lem24  7950  fin23lem26  7953  fin23lem23  7954  fin23lem22  7955  fin23lem19  7964  isfin1-3  8014  ttukeylem6  8143  brdom3  8155  brdom5  8156  brdom4  8157  imadomg  8161  fpwwe2lem12  8265  canthp1lem2  8277  wunin  8337  tskin  8383  gruima  8426  ingru  8439  gruina  8442  grur1a  8443  nqerf  8556  nqerrel  8558  hashun3  11368  hashdif  11377  rexanuz  11831  limsupgle  11953  rlimres  12034  lo1res  12035  lo1resb  12040  rlimresb  12041  o1resb  12042  lo1eq  12044  rlimeq  12045  o1of2  12088  o1rlimmul  12094  isercolllem2  12141  isercolllem3  12142  isercoll  12143  ackbijnn  12288  incexclem  12297  incexc  12298  bitsinvp1  12642  sadcaddlem  12650  sadadd2lem  12652  sadadd3  12654  sadaddlem  12659  sadasslem  12663  sadeq  12665  bitsres  12666  smuval2  12675  smupval  12681  smueqlem  12683  smumul  12686  prmreclem2  12966  ramub2  13063  ramub1lem2  13076  ressinbas  13206  ressress  13207  submre  13509  submrc  13532  isacs2  13557  isacs1i  13561  mreacs  13562  acsfn  13563  invss  13665  sscres  13702  coffth  13812  catcisolem  13940  catciso  13941  catcoppccl  13942  catcfuccl  13943  catcxpccl  13983  isdrs2  14075  isacs3lem  14271  isacs5lem  14274  acsfiindd  14282  psss  14325  psssdm2  14326  tsrss  14334  tsrdir  14362  resscntz  14809  sylow2a  14932  lsmmod  14986  frgpnabllem2  15164  gsumzres  15196  gsumzaddlem  15205  dprddisj2  15276  ablfac1eu  15310  ablfac2  15326  isunit  15441  lspextmo  15815  2idlval  15987  aspsubrg  16073  psrbagsn  16238  mplind  16245  zlpirlem2  16444  pjfval  16608  pjpm  16610  basdif0  16693  tgval2  16696  eltg3  16702  unitg  16707  tgcl  16709  tgdom  16718  tgidm  16720  ppttop  16746  epttop  16748  ntropn  16788  ntrin  16800  mretopd  16831  mreclatdemo  16835  restbas  16891  restfpw  16912  restcls  16913  ordtrest  16934  subbascn  16986  cncls  17005  cnpresti  17018  cnprest  17019  fincmp  17122  cmpsublem  17128  cmpsub  17129  fiuncmp  17133  indiscon  17146  connsub  17149  cnconn  17150  iunconlem  17155  clscon  17158  concompclo  17163  islly2  17212  cldllycmp  17223  kgentopon  17235  llycmpkgen2  17247  1stckgenlem  17250  ptbasfi  17278  txcls  17301  txcnp  17316  ptcnplem  17317  txcnmpt  17320  txcmplem2  17338  hausdiag  17341  txkgen  17348  xkopt  17351  xkococnlem  17355  txcon  17385  qtoptop2  17392  basqtop  17404  tgqtop  17405  kqnrmlem1  17436  kqnrmlem2  17437  nrmhmph  17487  fbssfi  17534  filin  17551  infil  17560  fbasrn  17581  fgtr  17587  ufprim  17606  flimrest  17680  hauspwpwf1  17684  txflf  17703  fclsrest  17721  alexsubALTlem3  17745  alexsubALTlem4  17746  ptcmplem5  17752  tsmsres  17828  tsmsxplem1  17837  xmetres  17930  metres  17931  blin2  17977  blbas  17978  blres  17979  setsmstopn  18026  met2ndci  18070  metrest  18072  ressxms  18073  tgioo  18304  xrsmopn  18320  zdis  18324  reconnlem1  18333  reconnlem2  18334  xrge0tsms  18341  cnheibor  18455  lebnum  18464  nmoleub2lem  18597  nmoleub2lem3  18598  nmoleub2lem2  18599  nmoleub3  18602  nmhmcn  18603  tchcph  18669  cfilresi  18723  cfilres  18724  caussi  18725  causs  18726  relcmpcmet  18744  minveclem4a  18796  minveclem4  18798  ismbl2  18888  cmmbl  18894  nulmbl2  18896  unmbl  18897  shftmbl  18898  volinun  18905  voliunlem1  18909  voliunlem2  18910  ioombl1lem4  18920  ioombl1  18921  ioorcl  18934  uniioombllem2  18940  uniioombllem3  18942  uniioombllem4  18943  uniioombllem5  18944  uniioombl  18946  volivth  18964  vitalilem3  18967  vitalilem4  18968  vitalilem5  18969  vitali  18970  mbfadd  19018  mbfsub  19019  i1fima2  19036  i1fd  19038  i1fadd  19052  itg1addlem2  19054  itg1addlem4  19056  itg1addlem5  19057  itg1climres  19071  mbfmul  19083  itg2splitlem  19105  itg2split  19106  limcresi  19237  limciun  19246  limcun  19247  dvreslem  19261  dvres2lem  19262  dvres  19263  dvres3a  19266  dvaddbr  19289  dvmulbr  19290  dvfsumle  19370  dvfsumabs  19372  ig1peu  19559  taylfvallem1  19738  tayl0  19743  pilem2  19830  pilem3  19831  rlimcnp2  20263  xrlimcnp  20265  ppisval  20343  ppifi  20345  ppiprm  20391  ppinprm  20392  chtprm  20393  chtnprm  20394  chtdif  20398  efchtdvds  20399  ppidif  20403  ppiltx  20417  prmorcht  20418  ppiub  20445  chtlepsi  20447  chtleppi  20451  pclogsum  20456  vmasum  20457  chpval2  20459  chpchtsum  20460  chpub  20461  2sqlem8  20613  chebbnd1lem1  20620  chtppilimlem1  20624  rplogsumlem2  20636  rpvmasum2  20663  dchrisum0re  20664  rplogsum  20678  dirith2  20679  opidon  20991  flddivrng  21084  phnv  21394  minvecolem2  21456  minvecolem3  21457  minvecolem5  21462  minvecolem6  21463  minvecolem7  21464  hlimcaui  21818  chdmm1i  22058  chabs1  22097  chabs2  22098  ledii  22117  lejdii  22119  pjoml4i  22168  cmbr3i  22181  cmbr4i  22182  cmm1i  22187  osumcor2i  22225  3oalem4  22246  pjssmii  22262  pjocini  22279  pjini  22280  mayete3i  22309  mayete3iOLD  22310  riesz4  22646  riesz1  22647  cnlnadjeui  22659  cnlnadjeu  22660  cnlnssadj  22662  nmopadjlei  22670  pjin1i  22774  pjclem1  22777  stji1i  22824  stm1i  22825  dmdbr2  22885  ssmd1  22893  mdslj2i  22902  mdsl2bi  22905  mdslmd1lem1  22907  mdslmd2i  22912  atomli  22964  atcvat4i  22979  sumdmdlem2  23001  dmdbr5ati  23004  dmdbr6ati  23005  dmdbr7ati  23006  infi  23031  ballotlemfelz  23051  ballotlemfp1  23052  infi1  23171  off2  23210  disjin  23364  xrge0tsmsd  23384  esumval  23427  esumel  23428  esumcst  23438  esumpcvgval  23448  esumcvg  23456  sigainb  23499  measinb2  23552  indf1ofs  23611  conpcon  23768  iccllyscon  23783  cvmsss2  23807  cvmcov2  23808  cvmopnlem  23811  cvmliftmolem2  23815  cvmliftlem15  23831  cvmlift2lem12  23847  nepss  24074  dedekindle  24085  dfon2lem4  24144  predss  24175  wfrlem4  24261  frrlem4  24286  nofulllem5  24362  txpss3v  24420  fixssdm  24448  fixssrn  24449  ontopbas  24869  domintrefb  25074  posprsr  25251  dfps2  25300  toplat  25301  reacomsmgrp1  25354  reacomsmgrp2  25355  reacomsmgrp3  25356  reacomsmgrp4  25357  clfsebsr  25360  resgcom  25362  clsint  25524  unint2t  25529  limptlimpr2lem2  25586  flfnei2  25588  islimrs4  25593  stfincomp  25602  lvsovso  25637  hdrmp  25717  inttaror  25911  fneer  26299  fnessref  26304  neibastop1  26319  neibastop2lem  26320  filnetlem3  26340  sstotbnd2  26509  ssbnd  26523  heibor1lem  26544  heiborlem1  26546  heiborlem3  26548  heiborlem5  26550  heiborlem6  26551  heiborlem10  26555  heibor  26556  exidcl  26577  elrfi  26780  elrfirn  26781  elrfirn2  26782  ismrcd1  26784  istopclsd  26786  isnacs2  26792  mrefg3  26794  isnacs3  26796  diophrw  26849  diophin  26863  aomclem2  27163  islmodfg  27178  lsmfgcl  27183  lmhmfgima  27193  lmhmfgsplit  27195  lmhmlnmsplit  27196  frlmsplit2  27254  pwfi2f1o  27271  hbt  27345  acsfn1p  27518  onfrALTlem2  28367  onfrALTlem2VD  28738  bnj1292  28921  lshpinN  29252  lcvexchlem5  29301  pmodlem2  30109  pmod1i  30110  pmodN  30112  osumcllem7N  30224  pexmidlem4N  30235  pl42lem3N  30243  djaclN  31399  dihoml4c  31639  dochdmj1  31653  djhcl  31663  dochexmidlem4  31726  mapd1o  31911  mapdin  31925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator