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

Theorem inss1 3700
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 3669 . . 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 3490 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1802    i^i cin 3457    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-ss 3472
This theorem is referenced by:  inss2  3701  ssinss1  3708  unabs  3710  nssinpss  3712  dfin4  3720  inv1  3794  disjdif  3882  uniintsn  4305  wefrc  4859  ordtri3or  4896  onfr  4903  ordelinel  4962  relin1  5106  resss  5283  resmpt3  5310  cnvcnvss  5447  funin  5641  funimass2  5648  fnresin1  5681  fnres  5683  fresin  5740  fresaun  5742  fresaunres2  5743  nfvres  5882  ssimaex  5919  fneqeql2  5977  funiunfv  6141  isoini2  6216  ofrfval  6529  ofval  6530  ofrval  6531  off  6535  ofres  6536  ofco  6541  fparlem3  6883  fparlem4  6884  smores  7021  smores2  7023  tfrlem5  7047  pmresg  7444  sbthlem7  7631  sbthcl  7637  infi  7741  imafi  7811  ixpfi2  7816  unifpw  7821  f1opwfi  7822  fival  7870  fi0  7878  dffi2  7881  elfiun  7888  dffi3  7889  marypha1lem  7891  ordtypelem3  7943  ordtypelem4  7944  ordtypelem6  7946  ordtypelem7  7947  ordtypelem8  7948  wdomima2g  8010  epfrs  8160  tskwe  8329  r0weon  8388  fodomfi2  8439  infpwfien  8441  ackbij1lem6  8603  ackbij1lem9  8606  ackbij1lem10  8607  ackbij1lem11  8608  ackbij1lem15  8612  ackbij1lem16  8613  fin23lem24  8700  fin23lem26  8703  fin23lem23  8704  fin23lem22  8705  fin23lem19  8714  isfin1-3  8764  ttukeylem6  8892  brdom3  8904  brdom5  8905  brdom4  8906  imadomg  8910  fpwwe2lem12  9017  canthp1lem2  9029  wunin  9089  tskin  9135  gruima  9178  ingru  9191  gruina  9194  grur1a  9195  nqerf  9306  nqerrel  9308  dedekindle  9743  hashun3  12426  hashdif  12450  rexanuz  13152  limsupgle  13274  rlimres  13355  lo1res  13356  lo1resb  13361  rlimresb  13362  o1resb  13363  lo1eq  13365  rlimeq  13366  o1of2  13409  o1rlimmul  13415  isercolllem2  13462  isercolllem3  13463  isercoll  13464  ackbijnn  13614  incexclem  13622  incexc  13623  bitsinvp1  13971  sadcaddlem  13979  sadadd2lem  13981  sadadd3  13983  sadaddlem  13988  sadasslem  13992  sadeq  13994  bitsres  13995  smuval2  14004  smupval  14010  smueqlem  14012  smumul  14015  prmreclem2  14307  ramub2  14404  ramub1lem2  14417  fvsetsid  14529  ressinbas  14565  ressress  14566  submre  14874  submrc  14897  isacs2  14922  isacs1i  14926  mreacs  14927  acsfn  14928  invss  15027  sscres  15064  coffth  15174  catcisolem  15302  catciso  15303  catcoppccl  15304  catcfuccl  15305  catcxpccl  15345  isdrs2  15437  isacs3lem  15665  isacs5lem  15668  acsfiindd  15676  psss  15713  psssdm2  15714  tsrss  15722  tsrdir  15737  resscntz  16238  sylow2a  16508  lsmmod  16562  frgpnabllem2  16747  gsumzres  16783  gsumzresOLD  16787  gsumzaddlem  16803  gsumzaddlemOLD  16805  dprddisj2  16955  dprddisj2OLD  16956  ablfac1eu  16992  ablfac2  17008  isunit  17174  lspextmo  17570  2idlval  17749  aspsubrg  17848  psrbagsn  18028  mplind  18035  zringlpirlem2  18377  zlpirlem2  18382  pjfval  18604  pjpm  18606  ofco2  18820  basdif0  19321  tgval2  19324  eltg3  19330  unitg  19335  tgcl  19337  tgdom  19346  tgidm  19348  ppttop  19374  epttop  19376  ntropn  19416  ntrin  19428  mretopd  19459  mreclatdemoBAD  19463  neiptoptop  19498  restbas  19525  restfpw  19546  neitr  19547  restcls  19548  ordtrest  19569  subbascn  19621  cncls  19641  cnpresti  19655  cnprest  19656  fincmp  19759  cmpsublem  19765  cmpsub  19766  fiuncmp  19770  indiscon  19785  connsub  19788  cnconn  19789  iunconlem  19794  clscon  19797  concompclo  19802  islly2  19851  cldllycmp  19862  kgentopon  19905  llycmpkgen2  19917  1stckgenlem  19920  ptbasfi  19948  txcls  19971  txcnp  19987  ptcnplem  19988  txcnmpt  19991  txcmplem2  20009  hausdiag  20012  txkgen  20019  xkopt  20022  xkococnlem  20026  txcon  20056  qtoptop2  20066  basqtop  20078  tgqtop  20079  kqnrmlem1  20110  kqnrmlem2  20111  nrmhmph  20161  fbssfi  20204  filin  20221  infil  20230  fbasrn  20251  fgtr  20257  ufprim  20276  flimrest  20350  hauspwpwf1  20354  txflf  20373  fclsrest  20391  alexsubALTlem3  20415  alexsubALTlem4  20416  ptcmplem5  20422  tsmsresOLD  20511  tsmsres  20512  tsmsxplem1  20521  ustund  20590  trust  20598  utoptop  20603  restutop  20606  cfiluweak  20664  xmetres  20733  metres  20734  blin2  20798  blbas  20799  blres  20800  setsmstopn  20847  met2ndci  20891  metrest  20893  ressxms  20894  tgioo  21167  xrsmopn  21183  zdis  21187  reconnlem1  21197  reconnlem2  21198  xrge0tsms  21205  cnheibor  21321  lebnum  21330  nmoleub2lem  21463  nmoleub2lem3  21464  nmoleub2lem2  21465  nmoleub3  21468  nmhmcn  21469  tchcph  21546  cfilresi  21600  cfilres  21601  caussi  21602  causs  21603  relcmpcmet  21621  minveclem4a  21711  minveclem4  21713  ismbl2  21804  cmmbl  21811  nulmbl2  21813  unmbl  21814  shftmbl  21815  volinun  21822  voliunlem1  21826  voliunlem2  21827  ioombl1lem4  21837  ioombl1  21838  ioorcl  21852  uniioombllem2  21858  uniioombllem3  21860  uniioombllem4  21861  uniioombllem5  21862  uniioombl  21864  volivth  21882  vitalilem3  21885  vitalilem4  21886  vitalilem5  21887  vitali  21888  mbfadd  21934  mbfsub  21935  i1fima2  21952  i1fd  21954  i1fadd  21968  itg1addlem2  21970  itg1addlem4  21972  itg1addlem5  21973  itg1climres  21987  mbfmul  21999  itg2splitlem  22021  itg2split  22022  limcresi  22155  limciun  22164  limcun  22165  dvreslem  22179  dvres2lem  22180  dvres  22181  dvres3a  22184  dvaddbr  22207  dvmulbr  22208  dvfsumle  22288  dvfsumabs  22290  ig1peu  22438  taylfvallem1  22617  tayl0  22622  pilem2  22712  pilem3  22713  rlimcnp2  23161  xrlimcnp  23163  ppisval  23242  ppifi  23244  ppiprm  23290  ppinprm  23291  chtprm  23292  chtnprm  23293  chtdif  23297  efchtdvds  23298  ppidif  23302  ppiltx  23316  prmorcht  23317  ppiub  23344  chtlepsi  23346  chtleppi  23350  pclogsum  23355  vmasum  23356  chpval2  23358  chpchtsum  23359  chpub  23360  2sqlem8  23512  chebbnd1lem1  23519  chtppilimlem1  23523  rplogsumlem2  23535  rpvmasum2  23562  dchrisum0re  23563  rplogsum  23577  dirith2  23578  axtgcgrrflx  23724  axtgcgrid  23725  axtgsegcon  23726  axtg5seg  23727  axtgbtwnid  23728  axtgpasch  23729  axtgcont1  23730  perpcom  23955  perpneq  23956  ragperp  23959  opidonOLD  25189  flddivrng  25282  phnv  25594  minvecolem2  25656  minvecolem3  25657  minvecolem5  25662  minvecolem6  25663  minvecolem7  25664  hlimcaui  26019  chdmm1i  26260  chabs1  26299  chabs2  26300  ledii  26319  lejdii  26321  pjoml4i  26370  cmbr3i  26383  cmbr4i  26384  cmm1i  26389  osumcor2i  26427  3oalem4  26448  pjssmii  26464  pjocini  26481  pjini  26482  mayete3i  26511  mayete3iOLD  26512  riesz4  26848  riesz1  26849  cnlnadjeui  26861  cnlnadjeu  26862  cnlnssadj  26864  nmopadjlei  26872  pjin1i  26976  pjclem1  26979  stji1i  27026  stm1i  27027  dmdbr2  27087  ssmd1  27095  mdslj2i  27104  mdsl2bi  27107  mdslmd1lem1  27109  mdslmd2i  27114  atomli  27166  atcvat4i  27181  sumdmdlem2  27203  dmdbr5ati  27206  dmdbr6ati  27207  dmdbr7ati  27208  disjin  27311  disjxpin  27312  imadifxp  27323  off2  27346  ffsrn  27417  xrge0tsmsd  27641  ordtrestNEW  27769  qqhnm  27837  qqhcn  27838  rrhre  27865  indf1ofs  27905  esumval  27923  esumel  27924  gsumesum  27933  esumlub  27934  esumcst  27937  esumfsup  27942  esumpcvgval  27950  esumcvg  27958  sigainb  28002  measinb2  28060  sibfinima  28147  sibfof  28148  eulerpartlemelr  28162  eulerpartlem1  28172  eulerpartgbij  28177  eulerpartlemgvv  28181  eulerpartlemgu  28182  eulerpartlemgs2  28185  sseqf  28197  ballotlemfelz  28295  ballotlemfp1  28296  conpcon  28546  iccllyscon  28561  cvmsss2  28585  cvmcov2  28586  cvmopnlem  28589  cvmliftmolem2  28593  cvmliftlem15  28609  cvmlift2lem12  28625  mvrsfpw  28732  msrf  28768  elmsta  28774  mthmpps  28808  nepss  28961  dfon2lem4  29186  predss  29219  wfrlem4  29314  frrlem4  29358  nofulllem5  29434  txpss3v  29496  fixssdm  29524  fixssrn  29525  limitssson  29529  ontopbas  29861  ptrest  30016  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  mbfposadd  30030  fneer  30139  neibastop1  30145  neibastop2lem  30146  filnetlem3  30166  sstotbnd2  30238  ssbnd  30252  heibor1lem  30273  heiborlem1  30275  heiborlem3  30277  heiborlem5  30279  heiborlem6  30280  heiborlem10  30284  heibor  30285  exidcl  30306  elrfi  30594  elrfirn  30595  elrfirn2  30596  ismrcd1  30598  istopclsd  30600  isnacs2  30606  mrefg3  30608  isnacs3  30610  diophrw  30660  diophin  30674  aomclem2  30969  islmodfg  30983  lsmfgcl  30988  lmhmfgima  30998  lmhmfgsplit  31000  lmhmlnmsplit  31001  pwfi2f1o  31012  hbt  31047  acsfn1p  31117  islptre  31529  sumnnodd  31540  limclner  31561  cncfuni  31592  fouriersw  31899  rngcbas  32492  rngchomfval  32493  rngccofval  32497  dfrngc2  32499  rnghmsscmap2  32500  rnghmsscmap  32501  rngcsect  32507  ringcbas  32532  ringchomfval  32533  ringccofval  32537  dfringc2  32539  rhmsscmap2  32540  rhmsscmap  32541  rhmsscrnghm  32547  ringcsect  32552  funcringcsetclem9  32564  fldc  32599  fldhmsubc  32600  rngcrescrhm  32601  rhmsubclem1  32602  fldcOLD  32618  fldhmsubcOLD  32619  rngcrescrhmOLD  32620  rhmsubcOLDlem1  32621  onfrALTlem2  33026  onfrALTlem2VD  33397  bnj1292  33581  bj-ablssgrp  34356  lshpinN  34416  lcvexchlem5  34465  pmodlem2  35273  pmod1i  35274  pmodN  35276  osumcllem7N  35388  pexmidlem4N  35399  pl42lem3N  35407  djaclN  36565  dihoml4c  36805  dochdmj1  36819  djhcl  36829  dochexmidlem4  36892  mapd1o  37077  mapdin  37091  taupilemrplb  37397  taupilem2  37399  taupi  37400  fiinfi  37423  xptrrel  37430  trrelind  37433  rp-imass  37444
  Copyright terms: Public domain W3C validator