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

Theorem inss1 3591
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 3560 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 460 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3381 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756    i^i cin 3348    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363
This theorem is referenced by:  inss2  3592  ssinss1  3599  unabs  3601  nssinpss  3603  dfin4  3611  inv1  3685  disjdif  3772  uniintsn  4186  wefrc  4735  ordtri3or  4772  onfr  4779  ordelinel  4838  relin1  4978  resss  5155  resmpt3  5178  cnvcnvss  5313  funin  5506  funimass2  5513  fnresin1  5546  fnres  5548  fresin  5601  fresaun  5603  fresaunres2  5604  nfvres  5741  ssimaex  5777  fneqeql2  5833  funiunfv  5986  isoini2  6051  ofrfval  6349  ofval  6350  ofrval  6351  off  6355  ofres  6356  ofco  6361  fparlem3  6695  fparlem4  6696  smores  6834  smores2  6836  tfrlem5  6860  pmresg  7261  sbthlem7  7448  sbthcl  7454  infi  7557  imafi  7625  ixpfi2  7630  unifpw  7635  f1opwfi  7636  fival  7683  fi0  7691  dffi2  7694  elfiun  7701  dffi3  7702  marypha1lem  7704  ordtypelem3  7755  ordtypelem4  7756  ordtypelem6  7758  ordtypelem7  7759  ordtypelem8  7760  wdomima2g  7822  epfrs  7972  tskwe  8141  r0weon  8200  fodomfi2  8251  infpwfien  8253  ackbij1lem6  8415  ackbij1lem9  8418  ackbij1lem10  8419  ackbij1lem11  8420  ackbij1lem15  8424  ackbij1lem16  8425  fin23lem24  8512  fin23lem26  8515  fin23lem23  8516  fin23lem22  8517  fin23lem19  8526  isfin1-3  8576  ttukeylem6  8704  brdom3  8716  brdom5  8717  brdom4  8718  imadomg  8722  fpwwe2lem12  8829  canthp1lem2  8841  wunin  8901  tskin  8947  gruima  8990  ingru  9003  gruina  9006  grur1a  9007  nqerf  9120  nqerrel  9122  dedekindle  9555  hashun3  12168  hashdif  12189  rexanuz  12854  limsupgle  12976  rlimres  13057  lo1res  13058  lo1resb  13063  rlimresb  13064  o1resb  13065  lo1eq  13067  rlimeq  13068  o1of2  13111  o1rlimmul  13117  isercolllem2  13164  isercolllem3  13165  isercoll  13166  ackbijnn  13312  incexclem  13320  incexc  13321  bitsinvp1  13666  sadcaddlem  13674  sadadd2lem  13676  sadadd3  13678  sadaddlem  13683  sadasslem  13687  sadeq  13689  bitsres  13690  smuval2  13699  smupval  13705  smueqlem  13707  smumul  13710  prmreclem2  13999  ramub2  14096  ramub1lem2  14109  fvsetsid  14220  ressinbas  14255  ressress  14256  submre  14564  submrc  14587  isacs2  14612  isacs1i  14616  mreacs  14617  acsfn  14618  invss  14720  sscres  14757  coffth  14867  catcisolem  14995  catciso  14996  catcoppccl  14997  catcfuccl  14998  catcxpccl  15038  isdrs2  15130  isacs3lem  15357  isacs5lem  15360  acsfiindd  15368  psss  15405  psssdm2  15406  tsrss  15414  tsrdir  15429  resscntz  15870  sylow2a  16139  lsmmod  16193  frgpnabllem2  16373  gsumzres  16409  gsumzresOLD  16413  gsumzaddlem  16429  gsumzaddlemOLD  16431  dprddisj2  16559  dprddisj2OLD  16560  ablfac1eu  16596  ablfac2  16612  isunit  16771  lspextmo  17159  2idlval  17337  aspsubrg  17424  psrbagsn  17599  mplind  17606  zringlpirlem2  17926  zlpirlem2  17931  pjfval  18153  pjpm  18155  ofco2  18354  basdif0  18580  tgval2  18583  eltg3  18589  unitg  18594  tgcl  18596  tgdom  18605  tgidm  18607  ppttop  18633  epttop  18635  ntropn  18675  ntrin  18687  mretopd  18718  mreclatdemoBAD  18722  neiptoptop  18757  restbas  18784  restfpw  18805  neitr  18806  restcls  18807  ordtrest  18828  subbascn  18880  cncls  18900  cnpresti  18914  cnprest  18915  fincmp  19018  cmpsublem  19024  cmpsub  19025  fiuncmp  19029  indiscon  19044  connsub  19047  cnconn  19048  iunconlem  19053  clscon  19056  concompclo  19061  islly2  19110  cldllycmp  19121  kgentopon  19133  llycmpkgen2  19145  1stckgenlem  19148  ptbasfi  19176  txcls  19199  txcnp  19215  ptcnplem  19216  txcnmpt  19219  txcmplem2  19237  hausdiag  19240  txkgen  19247  xkopt  19250  xkococnlem  19254  txcon  19284  qtoptop2  19294  basqtop  19306  tgqtop  19307  kqnrmlem1  19338  kqnrmlem2  19339  nrmhmph  19389  fbssfi  19432  filin  19449  infil  19458  fbasrn  19479  fgtr  19485  ufprim  19504  flimrest  19578  hauspwpwf1  19582  txflf  19601  fclsrest  19619  alexsubALTlem3  19643  alexsubALTlem4  19644  ptcmplem5  19650  tsmsresOLD  19739  tsmsres  19740  tsmsxplem1  19749  ustund  19818  trust  19826  utoptop  19831  restutop  19834  cfiluweak  19892  xmetres  19961  metres  19962  blin2  20026  blbas  20027  blres  20028  setsmstopn  20075  met2ndci  20119  metrest  20121  ressxms  20122  tgioo  20395  xrsmopn  20411  zdis  20415  reconnlem1  20425  reconnlem2  20426  xrge0tsms  20433  cnheibor  20549  lebnum  20558  nmoleub2lem  20691  nmoleub2lem3  20692  nmoleub2lem2  20693  nmoleub3  20696  nmhmcn  20697  tchcph  20774  cfilresi  20828  cfilres  20829  caussi  20830  causs  20831  relcmpcmet  20849  minveclem4a  20939  minveclem4  20941  ismbl2  21032  cmmbl  21038  nulmbl2  21040  unmbl  21041  shftmbl  21042  volinun  21049  voliunlem1  21053  voliunlem2  21054  ioombl1lem4  21064  ioombl1  21065  ioorcl  21079  uniioombllem2  21085  uniioombllem3  21087  uniioombllem4  21088  uniioombllem5  21089  uniioombl  21091  volivth  21109  vitalilem3  21112  vitalilem4  21113  vitalilem5  21114  vitali  21115  mbfadd  21161  mbfsub  21162  i1fima2  21179  i1fd  21181  i1fadd  21195  itg1addlem2  21197  itg1addlem4  21199  itg1addlem5  21200  itg1climres  21214  mbfmul  21226  itg2splitlem  21248  itg2split  21249  limcresi  21382  limciun  21391  limcun  21392  dvreslem  21406  dvres2lem  21407  dvres  21408  dvres3a  21411  dvaddbr  21434  dvmulbr  21435  dvfsumle  21515  dvfsumabs  21517  ig1peu  21665  taylfvallem1  21844  tayl0  21849  pilem2  21939  pilem3  21940  rlimcnp2  22382  xrlimcnp  22384  ppisval  22463  ppifi  22465  ppiprm  22511  ppinprm  22512  chtprm  22513  chtnprm  22514  chtdif  22518  efchtdvds  22519  ppidif  22523  ppiltx  22537  prmorcht  22538  ppiub  22565  chtlepsi  22567  chtleppi  22571  pclogsum  22576  vmasum  22577  chpval2  22579  chpchtsum  22580  chpub  22581  2sqlem8  22733  chebbnd1lem1  22740  chtppilimlem1  22744  rplogsumlem2  22756  rpvmasum2  22783  dchrisum0re  22784  rplogsum  22798  dirith2  22799  axtgcgrrflx  22945  axtgcgrid  22946  axtgsegcon  22947  axtg5seg  22948  axtgbtwnid  22949  axtgpasch  22950  axtgcont1  22951  perpcom  23126  perpneq  23127  ragperp  23130  opidon  23831  flddivrng  23924  phnv  24236  minvecolem2  24298  minvecolem3  24299  minvecolem5  24304  minvecolem6  24305  minvecolem7  24306  hlimcaui  24661  chdmm1i  24902  chabs1  24941  chabs2  24942  ledii  24961  lejdii  24963  pjoml4i  25012  cmbr3i  25025  cmbr4i  25026  cmm1i  25031  osumcor2i  25069  3oalem4  25090  pjssmii  25106  pjocini  25123  pjini  25124  mayete3i  25153  mayete3iOLD  25154  riesz4  25490  riesz1  25491  cnlnadjeui  25503  cnlnadjeu  25504  cnlnssadj  25506  nmopadjlei  25514  pjin1i  25618  pjclem1  25621  stji1i  25668  stm1i  25669  dmdbr2  25729  ssmd1  25737  mdslj2i  25746  mdsl2bi  25749  mdslmd1lem1  25751  mdslmd2i  25756  atomli  25808  atcvat4i  25823  sumdmdlem2  25845  dmdbr5ati  25848  dmdbr6ati  25849  dmdbr7ati  25850  disjin  25951  disjxpin  25952  imadifxp  25961  off2  25981  ffsrn  26051  gsumle  26268  xrge0tsmsd  26275  ordtrestNEW  26373  qqhnm  26441  qqhcn  26442  rrhre  26469  indf1ofs  26504  esumval  26522  esumel  26523  gsumesum  26532  esumlub  26533  esumcst  26536  esumfsup  26541  esumpcvgval  26549  esumcvg  26557  sigainb  26601  measunl  26652  measinb2  26659  sibfinima  26747  sibfof  26748  eulerpartlemelr  26762  eulerpartlem1  26772  eulerpartgbij  26777  eulerpartlemgvv  26781  eulerpartlemgu  26782  eulerpartlemgs2  26785  sseqf  26797  ballotlemfelz  26895  ballotlemfp1  26896  conpcon  27146  iccllyscon  27161  cvmsss2  27185  cvmcov2  27186  cvmopnlem  27189  cvmliftmolem2  27193  cvmliftlem15  27209  cvmlift2lem12  27225  nepss  27396  dfon2lem4  27621  predss  27654  wfrlem4  27749  frrlem4  27793  nofulllem5  27869  txpss3v  27931  fixssdm  27959  fixssrn  27960  limitssson  27964  ontopbas  28296  ptrest  28451  mblfinlem3  28456  mblfinlem4  28457  ismblfin  28458  mbfposadd  28465  fneer  28586  fnessref  28591  neibastop1  28606  neibastop2lem  28607  filnetlem3  28627  sstotbnd2  28699  ssbnd  28713  heibor1lem  28734  heiborlem1  28736  heiborlem3  28738  heiborlem5  28740  heiborlem6  28741  heiborlem10  28745  heibor  28746  exidcl  28767  elrfi  29056  elrfirn  29057  elrfirn2  29058  ismrcd1  29060  istopclsd  29062  isnacs2  29068  mrefg3  29070  isnacs3  29072  diophrw  29123  diophin  29137  aomclem2  29434  islmodfg  29448  lsmfgcl  29453  lmhmfgima  29463  lmhmfgsplit  29465  lmhmlnmsplit  29466  pwfi2f1o  29477  hbt  29512  acsfn1p  29582  onfrALTlem2  31350  onfrALTlem2VD  31721  bnj1292  31905  bj-ablssgrp  32670  lshpinN  32730  lcvexchlem5  32779  pmodlem2  33587  pmod1i  33588  pmodN  33590  osumcllem7N  33702  pexmidlem4N  33713  pl42lem3N  33721  djaclN  34877  dihoml4c  35117  dochdmj1  35131  djhcl  35141  dochexmidlem4  35204  mapd1o  35389  mapdin  35403  taupilemrplb  35710  taupilem2  35712  taupi  35713
  Copyright terms: Public domain W3C validator