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

Theorem inss1 3565
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 3534 . . 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 3355 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756    i^i cin 3322    C_ wss 3323
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 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337
This theorem is referenced by:  inss2  3566  ssinss1  3573  unabs  3575  nssinpss  3577  dfin4  3585  inv1  3659  disjdif  3746  uniintsn  4160  wefrc  4709  ordtri3or  4746  onfr  4753  ordelinel  4812  relin1  4952  resss  5129  resmpt3  5152  cnvcnvss  5287  funin  5480  funimass2  5487  fnresin1  5520  fnres  5522  fresin  5575  fresaun  5577  fresaunres2  5578  nfvres  5715  ssimaex  5751  fneqeql2  5807  funiunfv  5960  isoini2  6025  ofrfval  6323  ofval  6324  ofrval  6325  off  6329  ofres  6330  ofco  6335  fparlem3  6669  fparlem4  6670  smores  6805  smores2  6807  tfrlem5  6831  pmresg  7232  sbthlem7  7419  sbthcl  7425  infi  7528  imafi  7596  ixpfi2  7601  unifpw  7606  f1opwfi  7607  fival  7654  fi0  7662  dffi2  7665  elfiun  7672  dffi3  7673  marypha1lem  7675  ordtypelem3  7726  ordtypelem4  7727  ordtypelem6  7729  ordtypelem7  7730  ordtypelem8  7731  wdomima2g  7793  epfrs  7943  tskwe  8112  r0weon  8171  fodomfi2  8222  infpwfien  8224  ackbij1lem6  8386  ackbij1lem9  8389  ackbij1lem10  8390  ackbij1lem11  8391  ackbij1lem15  8395  ackbij1lem16  8396  fin23lem24  8483  fin23lem26  8486  fin23lem23  8487  fin23lem22  8488  fin23lem19  8497  isfin1-3  8547  ttukeylem6  8675  brdom3  8687  brdom5  8688  brdom4  8689  imadomg  8693  fpwwe2lem12  8800  canthp1lem2  8812  wunin  8872  tskin  8918  gruima  8961  ingru  8974  gruina  8977  grur1a  8978  nqerf  9091  nqerrel  9093  dedekindle  9526  hashun3  12139  hashdif  12160  rexanuz  12825  limsupgle  12947  rlimres  13028  lo1res  13029  lo1resb  13034  rlimresb  13035  o1resb  13036  lo1eq  13038  rlimeq  13039  o1of2  13082  o1rlimmul  13088  isercolllem2  13135  isercolllem3  13136  isercoll  13137  ackbijnn  13283  incexclem  13291  incexc  13292  bitsinvp1  13637  sadcaddlem  13645  sadadd2lem  13647  sadadd3  13649  sadaddlem  13654  sadasslem  13658  sadeq  13660  bitsres  13661  smuval2  13670  smupval  13676  smueqlem  13678  smumul  13681  prmreclem2  13970  ramub2  14067  ramub1lem2  14080  fvsetsid  14191  ressinbas  14226  ressress  14227  submre  14535  submrc  14558  isacs2  14583  isacs1i  14587  mreacs  14588  acsfn  14589  invss  14691  sscres  14728  coffth  14838  catcisolem  14966  catciso  14967  catcoppccl  14968  catcfuccl  14969  catcxpccl  15009  isdrs2  15101  isacs3lem  15328  isacs5lem  15331  acsfiindd  15339  psss  15376  psssdm2  15377  tsrss  15385  tsrdir  15400  resscntz  15840  sylow2a  16109  lsmmod  16163  frgpnabllem2  16343  gsumzres  16379  gsumzresOLD  16383  gsumzaddlem  16399  gsumzaddlemOLD  16401  dprddisj2  16525  dprddisj2OLD  16526  ablfac1eu  16562  ablfac2  16578  isunit  16737  lspextmo  17114  2idlval  17292  aspsubrg  17379  psrbagsn  17552  mplind  17559  zringlpirlem2  17879  zlpirlem2  17884  pjfval  18106  pjpm  18108  ofco2  18307  basdif0  18533  tgval2  18536  eltg3  18542  unitg  18547  tgcl  18549  tgdom  18558  tgidm  18560  ppttop  18586  epttop  18588  ntropn  18628  ntrin  18640  mretopd  18671  mreclatdemoBAD  18675  neiptoptop  18710  restbas  18737  restfpw  18758  neitr  18759  restcls  18760  ordtrest  18781  subbascn  18833  cncls  18853  cnpresti  18867  cnprest  18868  fincmp  18971  cmpsublem  18977  cmpsub  18978  fiuncmp  18982  indiscon  18997  connsub  19000  cnconn  19001  iunconlem  19006  clscon  19009  concompclo  19014  islly2  19063  cldllycmp  19074  kgentopon  19086  llycmpkgen2  19098  1stckgenlem  19101  ptbasfi  19129  txcls  19152  txcnp  19168  ptcnplem  19169  txcnmpt  19172  txcmplem2  19190  hausdiag  19193  txkgen  19200  xkopt  19203  xkococnlem  19207  txcon  19237  qtoptop2  19247  basqtop  19259  tgqtop  19260  kqnrmlem1  19291  kqnrmlem2  19292  nrmhmph  19342  fbssfi  19385  filin  19402  infil  19411  fbasrn  19432  fgtr  19438  ufprim  19457  flimrest  19531  hauspwpwf1  19535  txflf  19554  fclsrest  19572  alexsubALTlem3  19596  alexsubALTlem4  19597  ptcmplem5  19603  tsmsresOLD  19692  tsmsres  19693  tsmsxplem1  19702  ustund  19771  trust  19779  utoptop  19784  restutop  19787  cfiluweak  19845  xmetres  19914  metres  19915  blin2  19979  blbas  19980  blres  19981  setsmstopn  20028  met2ndci  20072  metrest  20074  ressxms  20075  tgioo  20348  xrsmopn  20364  zdis  20368  reconnlem1  20378  reconnlem2  20379  xrge0tsms  20386  cnheibor  20502  lebnum  20511  nmoleub2lem  20644  nmoleub2lem3  20645  nmoleub2lem2  20646  nmoleub3  20649  nmhmcn  20650  tchcph  20727  cfilresi  20781  cfilres  20782  caussi  20783  causs  20784  relcmpcmet  20802  minveclem4a  20892  minveclem4  20894  ismbl2  20985  cmmbl  20991  nulmbl2  20993  unmbl  20994  shftmbl  20995  volinun  21002  voliunlem1  21006  voliunlem2  21007  ioombl1lem4  21017  ioombl1  21018  ioorcl  21032  uniioombllem2  21038  uniioombllem3  21040  uniioombllem4  21041  uniioombllem5  21042  uniioombl  21044  volivth  21062  vitalilem3  21065  vitalilem4  21066  vitalilem5  21067  vitali  21068  mbfadd  21114  mbfsub  21115  i1fima2  21132  i1fd  21134  i1fadd  21148  itg1addlem2  21150  itg1addlem4  21152  itg1addlem5  21153  itg1climres  21167  mbfmul  21179  itg2splitlem  21201  itg2split  21202  limcresi  21335  limciun  21344  limcun  21345  dvreslem  21359  dvres2lem  21360  dvres  21361  dvres3a  21364  dvaddbr  21387  dvmulbr  21388  dvfsumle  21468  dvfsumabs  21470  ig1peu  21618  taylfvallem1  21797  tayl0  21802  pilem2  21892  pilem3  21893  rlimcnp2  22335  xrlimcnp  22337  ppisval  22416  ppifi  22418  ppiprm  22464  ppinprm  22465  chtprm  22466  chtnprm  22467  chtdif  22471  efchtdvds  22472  ppidif  22476  ppiltx  22490  prmorcht  22491  ppiub  22518  chtlepsi  22520  chtleppi  22524  pclogsum  22529  vmasum  22530  chpval2  22532  chpchtsum  22533  chpub  22534  2sqlem8  22686  chebbnd1lem1  22693  chtppilimlem1  22697  rplogsumlem2  22709  rpvmasum2  22736  dchrisum0re  22737  rplogsum  22751  dirith2  22752  axtgcgrrflx  22898  axtgcgrid  22899  axtgsegcon  22900  axtg5seg  22901  axtgbtwnid  22902  axtgpasch  22903  axtgcont1  22904  opidon  23760  flddivrng  23853  phnv  24165  minvecolem2  24227  minvecolem3  24228  minvecolem5  24233  minvecolem6  24234  minvecolem7  24235  hlimcaui  24590  chdmm1i  24831  chabs1  24870  chabs2  24871  ledii  24890  lejdii  24892  pjoml4i  24941  cmbr3i  24954  cmbr4i  24955  cmm1i  24960  osumcor2i  24998  3oalem4  25019  pjssmii  25035  pjocini  25052  pjini  25053  mayete3i  25082  mayete3iOLD  25083  riesz4  25419  riesz1  25420  cnlnadjeui  25432  cnlnadjeu  25433  cnlnssadj  25435  nmopadjlei  25443  pjin1i  25547  pjclem1  25550  stji1i  25597  stm1i  25598  dmdbr2  25658  ssmd1  25666  mdslj2i  25675  mdsl2bi  25678  mdslmd1lem1  25680  mdslmd2i  25685  atomli  25737  atcvat4i  25752  sumdmdlem2  25774  dmdbr5ati  25777  dmdbr6ati  25778  dmdbr7ati  25779  disjin  25880  disjxpin  25881  imadifxp  25890  off2  25910  ffsrn  25980  gsumle  26197  xrge0tsmsd  26204  ordtrestNEW  26303  qqhnm  26371  qqhcn  26372  rrhre  26399  indf1ofs  26434  esumval  26452  esumel  26453  gsumesum  26462  esumlub  26463  esumcst  26466  esumfsup  26471  esumpcvgval  26479  esumcvg  26487  sigainb  26531  measunl  26582  measinb2  26589  sibfinima  26677  sibfof  26678  eulerpartlemelr  26692  eulerpartlem1  26702  eulerpartgbij  26707  eulerpartlemgvv  26711  eulerpartlemgu  26712  eulerpartlemgs2  26715  sseqf  26727  ballotlemfelz  26825  ballotlemfp1  26826  conpcon  27076  iccllyscon  27091  cvmsss2  27115  cvmcov2  27116  cvmopnlem  27119  cvmliftmolem2  27123  cvmliftlem15  27139  cvmlift2lem12  27155  nepss  27325  dfon2lem4  27550  predss  27583  wfrlem4  27678  frrlem4  27722  nofulllem5  27798  txpss3v  27860  fixssdm  27888  fixssrn  27889  limitssson  27893  ontopbas  28226  ptrest  28378  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  mbfposadd  28392  fneer  28513  fnessref  28518  neibastop1  28533  neibastop2lem  28534  filnetlem3  28554  sstotbnd2  28626  ssbnd  28640  heibor1lem  28661  heiborlem1  28663  heiborlem3  28665  heiborlem5  28667  heiborlem6  28668  heiborlem10  28672  heibor  28673  exidcl  28694  elrfi  28983  elrfirn  28984  elrfirn2  28985  ismrcd1  28987  istopclsd  28989  isnacs2  28995  mrefg3  28997  isnacs3  28999  diophrw  29050  diophin  29064  aomclem2  29361  islmodfg  29375  lsmfgcl  29380  lmhmfgima  29390  lmhmfgsplit  29392  lmhmlnmsplit  29393  pwfi2f1o  29404  hbt  29439  acsfn1p  29509  onfrALTlem2  31141  onfrALTlem2VD  31512  bnj1292  31696  lshpinN  32474  lcvexchlem5  32523  pmodlem2  33331  pmod1i  33332  pmodN  33334  osumcllem7N  33446  pexmidlem4N  33457  pl42lem3N  33465  djaclN  34621  dihoml4c  34861  dochdmj1  34875  djhcl  34885  dochexmidlem4  34948  mapd1o  35133  mapdin  35147  taupilemrplb  35454  taupilem2  35456  taupi  35457
  Copyright terms: Public domain W3C validator