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

Theorem inss1 3711
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 3680 . . 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 3501 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762    i^i cin 3468    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ss 3483
This theorem is referenced by:  inss2  3712  ssinss1  3719  unabs  3721  nssinpss  3723  dfin4  3731  inv1  3805  disjdif  3892  uniintsn  4312  wefrc  4866  ordtri3or  4903  onfr  4910  ordelinel  4969  relin1  5111  resss  5288  resmpt3  5315  cnvcnvss  5452  funin  5646  funimass2  5653  fnresin1  5686  fnres  5688  fresin  5745  fresaun  5747  fresaunres2  5748  nfvres  5887  ssimaex  5923  fneqeql2  5981  funiunfv  6139  isoini2  6214  ofrfval  6523  ofval  6524  ofrval  6525  off  6529  ofres  6530  ofco  6535  fparlem3  6875  fparlem4  6876  smores  7013  smores2  7015  tfrlem5  7039  pmresg  7436  sbthlem7  7623  sbthcl  7629  infi  7733  imafi  7802  ixpfi2  7807  unifpw  7812  f1opwfi  7813  fival  7861  fi0  7869  dffi2  7872  elfiun  7879  dffi3  7880  marypha1lem  7882  ordtypelem3  7934  ordtypelem4  7935  ordtypelem6  7937  ordtypelem7  7938  ordtypelem8  7939  wdomima2g  8001  epfrs  8151  tskwe  8320  r0weon  8379  fodomfi2  8430  infpwfien  8432  ackbij1lem6  8594  ackbij1lem9  8597  ackbij1lem10  8598  ackbij1lem11  8599  ackbij1lem15  8603  ackbij1lem16  8604  fin23lem24  8691  fin23lem26  8694  fin23lem23  8695  fin23lem22  8696  fin23lem19  8705  isfin1-3  8755  ttukeylem6  8883  brdom3  8895  brdom5  8896  brdom4  8897  imadomg  8901  fpwwe2lem12  9008  canthp1lem2  9020  wunin  9080  tskin  9126  gruima  9169  ingru  9182  gruina  9185  grur1a  9186  nqerf  9297  nqerrel  9299  dedekindle  9733  hashun3  12407  hashdif  12428  rexanuz  13127  limsupgle  13249  rlimres  13330  lo1res  13331  lo1resb  13336  rlimresb  13337  o1resb  13338  lo1eq  13340  rlimeq  13341  o1of2  13384  o1rlimmul  13390  isercolllem2  13437  isercolllem3  13438  isercoll  13439  ackbijnn  13592  incexclem  13600  incexc  13601  bitsinvp1  13947  sadcaddlem  13955  sadadd2lem  13957  sadadd3  13959  sadaddlem  13964  sadasslem  13968  sadeq  13970  bitsres  13971  smuval2  13980  smupval  13986  smueqlem  13988  smumul  13991  prmreclem2  14283  ramub2  14380  ramub1lem2  14393  fvsetsid  14504  ressinbas  14540  ressress  14541  submre  14849  submrc  14872  isacs2  14897  isacs1i  14901  mreacs  14902  acsfn  14903  invss  15005  sscres  15042  coffth  15152  catcisolem  15280  catciso  15281  catcoppccl  15282  catcfuccl  15283  catcxpccl  15323  isdrs2  15415  isacs3lem  15642  isacs5lem  15645  acsfiindd  15653  psss  15690  psssdm2  15691  tsrss  15699  tsrdir  15714  resscntz  16157  sylow2a  16428  lsmmod  16482  frgpnabllem2  16662  gsumzres  16698  gsumzresOLD  16702  gsumzaddlem  16718  gsumzaddlemOLD  16720  dprddisj2  16870  dprddisj2OLD  16871  ablfac1eu  16907  ablfac2  16923  isunit  17083  lspextmo  17478  2idlval  17656  aspsubrg  17744  psrbagsn  17924  mplind  17931  zringlpirlem2  18270  zlpirlem2  18275  pjfval  18497  pjpm  18499  ofco2  18713  basdif0  19214  tgval2  19217  eltg3  19223  unitg  19228  tgcl  19230  tgdom  19239  tgidm  19241  ppttop  19267  epttop  19269  ntropn  19309  ntrin  19321  mretopd  19352  mreclatdemoBAD  19356  neiptoptop  19391  restbas  19418  restfpw  19439  neitr  19440  restcls  19441  ordtrest  19462  subbascn  19514  cncls  19534  cnpresti  19548  cnprest  19549  fincmp  19652  cmpsublem  19658  cmpsub  19659  fiuncmp  19663  indiscon  19678  connsub  19681  cnconn  19682  iunconlem  19687  clscon  19690  concompclo  19695  islly2  19744  cldllycmp  19755  kgentopon  19767  llycmpkgen2  19779  1stckgenlem  19782  ptbasfi  19810  txcls  19833  txcnp  19849  ptcnplem  19850  txcnmpt  19853  txcmplem2  19871  hausdiag  19874  txkgen  19881  xkopt  19884  xkococnlem  19888  txcon  19918  qtoptop2  19928  basqtop  19940  tgqtop  19941  kqnrmlem1  19972  kqnrmlem2  19973  nrmhmph  20023  fbssfi  20066  filin  20083  infil  20092  fbasrn  20113  fgtr  20119  ufprim  20138  flimrest  20212  hauspwpwf1  20216  txflf  20235  fclsrest  20253  alexsubALTlem3  20277  alexsubALTlem4  20278  ptcmplem5  20284  tsmsresOLD  20373  tsmsres  20374  tsmsxplem1  20383  ustund  20452  trust  20460  utoptop  20465  restutop  20468  cfiluweak  20526  xmetres  20595  metres  20596  blin2  20660  blbas  20661  blres  20662  setsmstopn  20709  met2ndci  20753  metrest  20755  ressxms  20756  tgioo  21029  xrsmopn  21045  zdis  21049  reconnlem1  21059  reconnlem2  21060  xrge0tsms  21067  cnheibor  21183  lebnum  21192  nmoleub2lem  21325  nmoleub2lem3  21326  nmoleub2lem2  21327  nmoleub3  21330  nmhmcn  21331  tchcph  21408  cfilresi  21462  cfilres  21463  caussi  21464  causs  21465  relcmpcmet  21483  minveclem4a  21573  minveclem4  21575  ismbl2  21666  cmmbl  21673  nulmbl2  21675  unmbl  21676  shftmbl  21677  volinun  21684  voliunlem1  21688  voliunlem2  21689  ioombl1lem4  21699  ioombl1  21700  ioorcl  21714  uniioombllem2  21720  uniioombllem3  21722  uniioombllem4  21723  uniioombllem5  21724  uniioombl  21726  volivth  21744  vitalilem3  21747  vitalilem4  21748  vitalilem5  21749  vitali  21750  mbfadd  21796  mbfsub  21797  i1fima2  21814  i1fd  21816  i1fadd  21830  itg1addlem2  21832  itg1addlem4  21834  itg1addlem5  21835  itg1climres  21849  mbfmul  21861  itg2splitlem  21883  itg2split  21884  limcresi  22017  limciun  22026  limcun  22027  dvreslem  22041  dvres2lem  22042  dvres  22043  dvres3a  22046  dvaddbr  22069  dvmulbr  22070  dvfsumle  22150  dvfsumabs  22152  ig1peu  22300  taylfvallem1  22479  tayl0  22484  pilem2  22574  pilem3  22575  rlimcnp2  23017  xrlimcnp  23019  ppisval  23098  ppifi  23100  ppiprm  23146  ppinprm  23147  chtprm  23148  chtnprm  23149  chtdif  23153  efchtdvds  23154  ppidif  23158  ppiltx  23172  prmorcht  23173  ppiub  23200  chtlepsi  23202  chtleppi  23206  pclogsum  23211  vmasum  23212  chpval2  23214  chpchtsum  23215  chpub  23216  2sqlem8  23368  chebbnd1lem1  23375  chtppilimlem1  23379  rplogsumlem2  23391  rpvmasum2  23418  dchrisum0re  23419  rplogsum  23433  dirith2  23434  axtgcgrrflx  23580  axtgcgrid  23581  axtgsegcon  23582  axtg5seg  23583  axtgbtwnid  23584  axtgpasch  23585  axtgcont1  23586  perpcom  23791  perpneq  23792  ragperp  23795  opidon  24986  flddivrng  25079  phnv  25391  minvecolem2  25453  minvecolem3  25454  minvecolem5  25459  minvecolem6  25460  minvecolem7  25461  hlimcaui  25816  chdmm1i  26057  chabs1  26096  chabs2  26097  ledii  26116  lejdii  26118  pjoml4i  26167  cmbr3i  26180  cmbr4i  26181  cmm1i  26186  osumcor2i  26224  3oalem4  26245  pjssmii  26261  pjocini  26278  pjini  26279  mayete3i  26308  mayete3iOLD  26309  riesz4  26645  riesz1  26646  cnlnadjeui  26658  cnlnadjeu  26659  cnlnssadj  26661  nmopadjlei  26669  pjin1i  26773  pjclem1  26776  stji1i  26823  stm1i  26824  dmdbr2  26884  ssmd1  26892  mdslj2i  26901  mdsl2bi  26904  mdslmd1lem1  26906  mdslmd2i  26911  atomli  26963  atcvat4i  26978  sumdmdlem2  27000  dmdbr5ati  27003  dmdbr6ati  27004  dmdbr7ati  27005  disjin  27105  disjxpin  27106  imadifxp  27117  off2  27140  ffsrn  27210  xrge0tsmsd  27424  ordtrestNEW  27525  qqhnm  27593  qqhcn  27594  rrhre  27621  indf1ofs  27665  esumval  27683  esumel  27684  gsumesum  27693  esumlub  27694  esumcst  27697  esumfsup  27702  esumpcvgval  27710  esumcvg  27718  sigainb  27762  measunl  27813  measinb2  27820  sibfinima  27907  sibfof  27908  eulerpartlemelr  27922  eulerpartlem1  27932  eulerpartgbij  27937  eulerpartlemgvv  27941  eulerpartlemgu  27942  eulerpartlemgs2  27945  sseqf  27957  ballotlemfelz  28055  ballotlemfp1  28056  conpcon  28306  iccllyscon  28321  cvmsss2  28345  cvmcov2  28346  cvmopnlem  28349  cvmliftmolem2  28353  cvmliftlem15  28369  cvmlift2lem12  28385  nepss  28556  dfon2lem4  28781  predss  28814  wfrlem4  28909  frrlem4  28953  nofulllem5  29029  txpss3v  29091  fixssdm  29119  fixssrn  29120  limitssson  29124  ontopbas  29456  ptrest  29612  mblfinlem3  29617  mblfinlem4  29618  ismblfin  29619  mbfposadd  29626  fneer  29747  fnessref  29752  neibastop1  29767  neibastop2lem  29768  filnetlem3  29788  sstotbnd2  29860  ssbnd  29874  heibor1lem  29895  heiborlem1  29897  heiborlem3  29899  heiborlem5  29901  heiborlem6  29902  heiborlem10  29906  heibor  29907  exidcl  29928  elrfi  30217  elrfirn  30218  elrfirn2  30219  ismrcd1  30221  istopclsd  30223  isnacs2  30229  mrefg3  30231  isnacs3  30233  diophrw  30283  diophin  30297  aomclem2  30594  islmodfg  30608  lsmfgcl  30613  lmhmfgima  30623  lmhmfgsplit  30625  lmhmlnmsplit  30626  pwfi2f1o  30637  hbt  30672  acsfn1p  30742  islptre  31116  sumnnodd  31127  limclner  31148  cncfuni  31180  fouriersw  31487  onfrALTlem2  32273  onfrALTlem2VD  32644  bnj1292  32828  bj-ablssgrp  33601  lshpinN  33661  lcvexchlem5  33710  pmodlem2  34518  pmod1i  34519  pmodN  34521  osumcllem7N  34633  pexmidlem4N  34644  pl42lem3N  34652  djaclN  35808  dihoml4c  36048  dochdmj1  36062  djhcl  36072  dochexmidlem4  36135  mapd1o  36320  mapdin  36334  taupilemrplb  36641  taupilem2  36643  taupi  36644  fiinfi  36653  xptrrel  36660  trrelind  36663  rp-imass  36671
  Copyright terms: Public domain W3C validator