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

Theorem inss1 3296
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
StepHypRef Expression
1 elin 3266 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 448 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3105 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    i^i cin 3077    C_ wss 3078
This theorem is referenced by:  inss2  3297  ssinss1  3304  unabs  3306  nssinpss  3308  dfin4  3316  inv1  3388  disjdif  3432  uniintsn  3797  epse  4269  wefrc  4280  ordtri3or  4317  onfr  4324  relin1  4710  resss  4886  resmpt3  4908  cnvcnvss  5035  funin  5176  funimass2  5183  fnresin1  5215  fnres  5217  fresin  5267  fresaun  5269  fresaunres2  5270  nfvres  5409  ssimaex  5436  fneqeql2  5486  funiunfv  5626  isoini2  5688  ofrfval  5938  ofval  5939  ofrval  5940  off  5945  ofres  5946  ofco  5949  fparlem3  6072  fparlem4  6073  smores  6255  smores2  6257  pmresg  6681  sbthlem7  6862  sbthcl  6868  imafi  7032  ixpfi2  7038  unifpw  7042  f1opwfi  7043  fival  7050  fi0  7057  dffi2  7060  elfiun  7067  dffi3  7068  marypha1lem  7070  ordtypelem3  7119  ordtypelem4  7120  ordtypelem6  7122  ordtypelem7  7123  ordtypelem8  7124  wdomima2g  7184  epfrs  7297  tskwe  7467  r0weon  7524  fodomfi2  7571  infpwfien  7573  ackbij1lem6  7735  ackbij1lem9  7738  ackbij1lem10  7739  ackbij1lem11  7740  ackbij1lem15  7744  ackbij1lem16  7745  fin23lem24  7832  fin23lem26  7835  fin23lem23  7836  fin23lem22  7837  fin23lem19  7846  isfin1-3  7896  ttukeylem6  8025  brdom3  8037  brdom5  8038  brdom4  8039  imadomg  8043  fpwwe2lem12  8143  canthp1lem2  8155  wunin  8215  tskin  8261  gruima  8304  ingru  8317  gruina  8320  grur1a  8321  nqerf  8434  nqerrel  8436  hashdif  11252  rexanuz  11706  limsupgle  11828  rlimres  11909  lo1res  11910  lo1resb  11915  rlimresb  11916  o1resb  11917  lo1eq  11919  rlimeq  11920  o1of2  11963  o1rlimmul  11969  isercolllem2  12016  isercolllem3  12017  isercoll  12018  ackbijnn  12163  bitsinvp1  12514  sadcaddlem  12522  sadadd2lem  12524  sadadd3  12526  sadaddlem  12531  sadasslem  12535  sadeq  12537  bitsres  12538  smuval2  12547  smupval  12553  smueqlem  12555  smumul  12558  prmreclem2  12838  ramub2  12935  ramub1lem2  12948  ressinbas  13078  ressress  13079  submre  13379  submrc  13397  isacs2  13400  isacs1i  13403  mreacs  13404  acsfn  13405  invss  13507  sscres  13544  coffth  13654  catcisolem  13782  catciso  13783  catcoppccl  13784  catcfuccl  13785  catcxpccl  13825  isdrs2  13917  isacs3lem  14113  isacs5lem  14116  psss  14158  psssdm2  14159  tsrss  14167  tsrdir  14195  resscntz  14642  sylow2a  14765  lsmmod  14819  frgpnabllem2  14997  gsumzres  15029  gsumzaddlem  15038  dprddisj2  15109  ablfac1eu  15143  ablfac2  15159  isunit  15274  lspextmo  15648  2idlval  15817  aspsubrg  15903  psrbagsn  16068  mplind  16075  zlpirlem2  16274  pjfval  16438  pjpm  16440  basdif0  16523  tgval2  16526  eltg3  16532  unitg  16537  tgcl  16539  tgdom  16548  tgidm  16550  ppttop  16576  epttop  16578  ntropn  16618  ntrin  16630  mretopd  16661  mreclatdemo  16665  restbas  16721  restfpw  16742  restcls  16743  ordtrest  16764  subbascn  16816  cncls  16835  cnpresti  16848  cnprest  16849  fincmp  16952  cmpsublem  16958  cmpsub  16959  fiuncmp  16963  indiscon  16976  connsub  16979  cnconn  16980  iunconlem  16985  clscon  16988  concompclo  16993  islly2  17042  cldllycmp  17053  kgentopon  17065  llycmpkgen2  17077  1stckgenlem  17080  ptbasfi  17108  txcls  17131  txcnp  17146  ptcnplem  17147  txcnmpt  17150  txcmplem2  17168  hausdiag  17171  txkgen  17178  xkopt  17181  xkococnlem  17185  txcon  17215  qtoptop2  17222  basqtop  17234  tgqtop  17235  kqnrmlem1  17266  kqnrmlem2  17267  nrmhmph  17317  fbssfi  17364  filin  17381  infil  17390  fbasrn  17411  fgtr  17417  ufprim  17436  flimrest  17510  hauspwpwf1  17514  txflf  17533  fclsrest  17551  alexsubALTlem3  17575  alexsubALTlem4  17576  ptcmplem5  17582  tsmsres  17658  tsmsxplem1  17667  xmetres  17760  metres  17761  blin2  17807  blbas  17808  blres  17809  setsmstopn  17856  met2ndci  17900  metrest  17902  ressxms  17903  tgioo  18134  xrsmopn  18150  zdis  18154  reconnlem1  18163  reconnlem2  18164  xrge0tsms  18171  cnheibor  18285  lebnum  18294  nmoleub2lem  18427  nmoleub2lem3  18428  nmoleub2lem2  18429  nmoleub3  18432  nmhmcn  18433  tchcph  18499  cfilresi  18553  cfilres  18554  caussi  18555  causs  18556  relcmpcmet  18574  minveclem4a  18626  minveclem4  18628  ismbl2  18718  cmmbl  18724  nulmbl2  18726  unmbl  18727  shftmbl  18728  volinun  18735  voliunlem1  18739  voliunlem2  18740  ioombl1lem4  18750  ioombl1  18751  ioorcl  18764  uniioombllem2  18770  uniioombllem3  18772  uniioombllem4  18773  uniioombllem5  18774  uniioombl  18776  volivth  18794  vitalilem3  18797  vitalilem4  18798  vitalilem5  18799  vitali  18800  mbfadd  18848  mbfsub  18849  i1fima2  18866  i1fd  18868  i1fadd  18882  itg1addlem2  18884  itg1addlem4  18886  itg1addlem5  18887  itg1climres  18901  mbfmul  18913  itg2splitlem  18935  itg2split  18936  limcresi  19067  limciun  19076  limcun  19077  dvreslem  19091  dvres2lem  19092  dvres  19093  dvres3a  19096  dvaddbr  19119  dvmulbr  19120  dvfsumle  19200  dvfsumabs  19202  ig1peu  19389  taylfvallem1  19568  tayl0  19573  pilem2  19660  pilem3  19661  rlimcnp2  20093  xrlimcnp  20095  ppisval  20173  ppifi  20175  ppiprm  20221  ppinprm  20222  chtprm  20223  chtnprm  20224  chtdif  20228  efchtdvds  20229  ppidif  20233  ppiltx  20247  prmorcht  20248  ppiub  20275  chtlepsi  20277  chtleppi  20281  pclogsum  20286  vmasum  20287  chpval2  20289  chpchtsum  20290  chpub  20291  2sqlem8  20443  chebbnd1lem1  20450  chtppilimlem1  20454  rplogsumlem2  20466  rpvmasum2  20493  dchrisum0re  20494  rplogsum  20508  dirith2  20509  opidon  20819  flddivrng  20912  phnv  21222  minvecolem2  21284  minvecolem3  21285  minvecolem5  21290  minvecolem6  21291  minvecolem7  21292  hlimcaui  21646  chdmm1i  21886  chabs1  21925  chabs2  21926  ledii  21945  lejdii  21947  pjoml4i  22014  cmbr3i  22027  cmbr4i  22028  cmm1i  22033  osumcor2i  22071  3oalem4  22092  pjssmii  22108  pjocini  22125  pjini  22126  mayete3i  22155  mayete3iOLD  22156  riesz4  22474  riesz1  22475  cnlnadjeui  22487  cnlnadjeu  22488  cnlnssadj  22490  nmopadjlei  22498  pjin1i  22602  pjclem1  22605  stji1i  22652  stm1i  22653  dmdbr2  22713  ssmd1  22721  mdslj2i  22730  mdsl2bi  22733  mdslmd1lem1  22735  mdslmd2i  22740  atomli  22792  atcvat4i  22807  sumdmdlem2  22829  dmdbr5ati  22832  dmdbr6ati  22833  dmdbr7ati  22834  conpcon  22937  iccllyscon  22952  cvmsss2  22976  cvmcov2  22977  cvmopnlem  22980  cvmliftmolem2  22984  cvmliftlem15  23000  cvmlift2lem12  23016  nepss  23243  dedekindle  23253  dfon2lem4  23310  predss  23341  wfrlem4  23427  frrlem4  23452  txpss3v  23593  fixssdm  23621  fixssrn  23622  ontopbas  24041  domintrefb  24228  posprsr  24406  dfps2  24455  toplat  24456  reacomsmgrp1  24509  reacomsmgrp2  24510  reacomsmgrp3  24511  reacomsmgrp4  24512  clfsebsr  24515  resgcom  24517  clsint  24679  unint2t  24684  limptlimpr2lem2  24741  flfnei2  24743  islimrs4  24748  stfincomp  24757  lvsovso  24792  hdrmp  24872  inttaror  25066  fneer  25454  fnessref  25459  neibastop1  25474  neibastop2lem  25475  filnetlem3  25495  sstotbnd2  25664  ssbnd  25678  heibor1lem  25699  heiborlem1  25701  heiborlem3  25703  heiborlem5  25705  heiborlem6  25706  heiborlem10  25710  heibor  25711  exidcl  25732  elrfi  25935  elrfirn  25936  elrfirn2  25937  ismrcd1  25939  istopclsd  25941  isnacs2  25947  mrefg3  25949  isnacs3  25951  diophrw  26004  diophin  26018  aomclem2  26318  islmodfg  26333  lsmfgcl  26338  lmhmfgima  26348  lmhmfgsplit  26350  lmhmlnmsplit  26351  frlmsplit2  26409  pwfi2f1o  26426  hbt  26500  acsfn1p  26673  onfrALTlem2  27004  onfrALTlem2VD  27355  bnj1292  27537  lshpinN  27868  lcvexchlem5  27917  pmodlem2  28725  pmod1i  28726  pmodN  28728  osumcllem7N  28840  pexmidlem4N  28851  pl42lem3N  28859  djaclN  30015  dihoml4c  30255  dochdmj1  30269  djhcl  30279  dochexmidlem4  30342  mapd1o  30527  mapdin  30541
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator