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

Theorem inss1 3521
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 3490 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 447 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3312 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721    i^i cin 3279    C_ wss 3280
This theorem is referenced by:  inss2  3522  ssinss1  3529  unabs  3531  nssinpss  3533  dfin4  3541  inv1  3614  disjdif  3660  uniintsn  4047  wefrc  4536  ordtri3or  4573  onfr  4580  ordelinel  4639  relin1  4951  resss  5129  resmpt3  5151  cnvcnvss  5284  funin  5479  funimass2  5486  fnresin1  5518  fnres  5520  fresin  5571  fresaun  5573  fresaunres2  5574  nfvres  5719  ssimaex  5747  fneqeql2  5798  funiunfv  5954  isoini2  6018  ofrfval  6272  ofval  6273  ofrval  6274  off  6279  ofres  6280  ofco  6283  fparlem3  6407  fparlem4  6408  smores  6573  smores2  6575  pmresg  7000  sbthlem7  7182  sbthcl  7188  infi  7291  imafi  7357  ixpfi2  7363  unifpw  7367  f1opwfi  7368  fival  7375  fi0  7383  dffi2  7386  elfiun  7393  dffi3  7394  marypha1lem  7396  ordtypelem3  7445  ordtypelem4  7446  ordtypelem6  7448  ordtypelem7  7449  ordtypelem8  7450  wdomima2g  7510  epfrs  7623  tskwe  7793  r0weon  7850  fodomfi2  7897  infpwfien  7899  ackbij1lem6  8061  ackbij1lem9  8064  ackbij1lem10  8065  ackbij1lem11  8066  ackbij1lem15  8070  ackbij1lem16  8071  fin23lem24  8158  fin23lem26  8161  fin23lem23  8162  fin23lem22  8163  fin23lem19  8172  isfin1-3  8222  ttukeylem6  8350  brdom3  8362  brdom5  8363  brdom4  8364  imadomg  8368  fpwwe2lem12  8472  canthp1lem2  8484  wunin  8544  tskin  8590  gruima  8633  ingru  8646  gruina  8649  grur1a  8650  nqerf  8763  nqerrel  8765  hashun3  11613  hashdif  11633  rexanuz  12104  limsupgle  12226  rlimres  12307  lo1res  12308  lo1resb  12313  rlimresb  12314  o1resb  12315  lo1eq  12317  rlimeq  12318  o1of2  12361  o1rlimmul  12367  isercolllem2  12414  isercolllem3  12415  isercoll  12416  ackbijnn  12562  incexclem  12571  incexc  12572  bitsinvp1  12916  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  sadasslem  12937  sadeq  12939  bitsres  12940  smuval2  12949  smupval  12955  smueqlem  12957  smumul  12960  prmreclem2  13240  ramub2  13337  ramub1lem2  13350  ressinbas  13480  ressress  13481  submre  13785  submrc  13808  isacs2  13833  isacs1i  13837  mreacs  13838  acsfn  13839  invss  13941  sscres  13978  coffth  14088  catcisolem  14216  catciso  14217  catcoppccl  14218  catcfuccl  14219  catcxpccl  14259  isdrs2  14351  isacs3lem  14547  isacs5lem  14550  acsfiindd  14558  psss  14601  psssdm2  14602  tsrss  14610  tsrdir  14638  resscntz  15085  sylow2a  15208  lsmmod  15262  frgpnabllem2  15440  gsumzres  15472  gsumzaddlem  15481  dprddisj2  15552  ablfac1eu  15586  ablfac2  15602  isunit  15717  lspextmo  16087  2idlval  16259  aspsubrg  16345  psrbagsn  16510  mplind  16517  zlpirlem2  16724  pjfval  16888  pjpm  16890  basdif0  16973  tgval2  16976  eltg3  16982  unitg  16987  tgcl  16989  tgdom  16998  tgidm  17000  ppttop  17026  epttop  17028  ntropn  17068  ntrin  17080  mretopd  17111  mreclatdemo  17115  neiptoptop  17150  restbas  17176  restfpw  17197  neitr  17198  restcls  17199  ordtrest  17220  subbascn  17272  cncls  17292  cnpresti  17306  cnprest  17307  fincmp  17410  cmpsublem  17416  cmpsub  17417  fiuncmp  17421  indiscon  17434  connsub  17437  cnconn  17438  iunconlem  17443  clscon  17446  concompclo  17451  islly2  17500  cldllycmp  17511  kgentopon  17523  llycmpkgen2  17535  1stckgenlem  17538  ptbasfi  17566  txcls  17589  txcnp  17605  ptcnplem  17606  txcnmpt  17609  txcmplem2  17627  hausdiag  17630  txkgen  17637  xkopt  17640  xkococnlem  17644  txcon  17674  qtoptop2  17684  basqtop  17696  tgqtop  17697  kqnrmlem1  17728  kqnrmlem2  17729  nrmhmph  17779  fbssfi  17822  filin  17839  infil  17848  fbasrn  17869  fgtr  17875  ufprim  17894  flimrest  17968  hauspwpwf1  17972  txflf  17991  fclsrest  18009  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem5  18040  tsmsres  18126  tsmsxplem1  18135  ustund  18204  trust  18212  utoptop  18217  restutop  18220  cfiluweak  18278  xmetres  18347  metres  18348  blin2  18412  blbas  18413  blres  18414  setsmstopn  18461  met2ndci  18505  metrest  18507  ressxms  18508  tgioo  18780  xrsmopn  18796  zdis  18800  reconnlem1  18810  reconnlem2  18811  xrge0tsms  18818  cnheibor  18933  lebnum  18942  nmoleub2lem  19075  nmoleub2lem3  19076  nmoleub2lem2  19077  nmoleub3  19080  nmhmcn  19081  tchcph  19147  cfilresi  19201  cfilres  19202  caussi  19203  causs  19204  relcmpcmet  19222  minveclem4a  19284  minveclem4  19286  ismbl2  19376  cmmbl  19382  nulmbl2  19384  unmbl  19385  shftmbl  19386  volinun  19393  voliunlem1  19397  voliunlem2  19398  ioombl1lem4  19408  ioombl1  19409  ioorcl  19422  uniioombllem2  19428  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  volivth  19452  vitalilem3  19455  vitalilem4  19456  vitalilem5  19457  vitali  19458  mbfadd  19506  mbfsub  19507  i1fima2  19524  i1fd  19526  i1fadd  19540  itg1addlem2  19542  itg1addlem4  19544  itg1addlem5  19545  itg1climres  19559  mbfmul  19571  itg2splitlem  19593  itg2split  19594  limcresi  19725  limciun  19734  limcun  19735  dvreslem  19749  dvres2lem  19750  dvres  19751  dvres3a  19754  dvaddbr  19777  dvmulbr  19778  dvfsumle  19858  dvfsumabs  19860  ig1peu  20047  taylfvallem1  20226  tayl0  20231  pilem2  20321  pilem3  20322  rlimcnp2  20758  xrlimcnp  20760  ppisval  20839  ppifi  20841  ppiprm  20887  ppinprm  20888  chtprm  20889  chtnprm  20890  chtdif  20894  efchtdvds  20895  ppidif  20899  ppiltx  20913  prmorcht  20914  ppiub  20941  chtlepsi  20943  chtleppi  20947  pclogsum  20952  vmasum  20953  chpval2  20955  chpchtsum  20956  chpub  20957  2sqlem8  21109  chebbnd1lem1  21116  chtppilimlem1  21120  rplogsumlem2  21132  rpvmasum2  21159  dchrisum0re  21160  rplogsum  21174  dirith2  21175  opidon  21863  flddivrng  21956  phnv  22268  minvecolem2  22330  minvecolem3  22331  minvecolem5  22336  minvecolem6  22337  minvecolem7  22338  hlimcaui  22692  chdmm1i  22932  chabs1  22971  chabs2  22972  ledii  22991  lejdii  22993  pjoml4i  23042  cmbr3i  23055  cmbr4i  23056  cmm1i  23061  osumcor2i  23099  3oalem4  23120  pjssmii  23136  pjocini  23153  pjini  23154  mayete3i  23183  mayete3iOLD  23184  riesz4  23520  riesz1  23521  cnlnadjeui  23533  cnlnadjeu  23534  cnlnssadj  23536  nmopadjlei  23544  pjin1i  23648  pjclem1  23651  stji1i  23698  stm1i  23699  dmdbr2  23759  ssmd1  23767  mdslj2i  23776  mdsl2bi  23779  mdslmd1lem1  23781  mdslmd2i  23786  atomli  23838  atcvat4i  23853  sumdmdlem2  23875  dmdbr5ati  23878  dmdbr6ati  23879  dmdbr7ati  23880  disjin  23980  disjxpin  23981  imadifxp  23991  off2  24007  xrge0tsmsd  24176  qqhnm  24327  qqhcn  24328  rrhre  24340  indf1ofs  24376  esumval  24394  esumel  24395  gsumesum  24404  esumlub  24405  esumcst  24408  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  sigainb  24472  measunl  24523  measinb2  24530  sibfof  24607  ballotlemfelz  24701  ballotlemfp1  24702  conpcon  24875  iccllyscon  24890  cvmsss2  24914  cvmcov2  24915  cvmopnlem  24918  cvmliftmolem2  24922  cvmliftlem15  24938  cvmlift2lem12  24954  nepss  25128  dedekindle  25141  dfon2lem4  25356  predss  25387  wfrlem4  25473  frrlem4  25498  nofulllem5  25574  txpss3v  25632  fixssdm  25660  fixssrn  25661  ontopbas  26082  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfposadd  26153  fneer  26258  fnessref  26263  neibastop1  26278  neibastop2lem  26279  filnetlem3  26299  sstotbnd2  26373  ssbnd  26387  heibor1lem  26408  heiborlem1  26410  heiborlem3  26412  heiborlem5  26414  heiborlem6  26415  heiborlem10  26419  heibor  26420  exidcl  26441  elrfi  26638  elrfirn  26639  elrfirn2  26640  ismrcd1  26642  istopclsd  26644  isnacs2  26650  mrefg3  26652  isnacs3  26654  diophrw  26707  diophin  26721  aomclem2  27020  islmodfg  27035  lsmfgcl  27040  lmhmfgima  27050  lmhmfgsplit  27052  lmhmlnmsplit  27053  frlmsplit2  27111  pwfi2f1o  27128  hbt  27202  acsfn1p  27375  onfrALTlem2  28343  onfrALTlem2VD  28710  bnj1292  28893  lshpinN  29472  lcvexchlem5  29521  pmodlem2  30329  pmod1i  30330  pmodN  30332  osumcllem7N  30444  pexmidlem4N  30455  pl42lem3N  30463  djaclN  31619  dihoml4c  31859  dochdmj1  31873  djhcl  31883  dochexmidlem4  31946  mapd1o  32131  mapdin  32145
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator