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

Theorem inss1 3723
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 3692 . . 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 3513 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767    i^i cin 3480    C_ wss 3481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-in 3488  df-ss 3495
This theorem is referenced by:  inss2  3724  ssinss1  3731  unabs  3733  nssinpss  3735  dfin4  3743  inv1  3817  disjdif  3905  uniintsn  4325  wefrc  4879  ordtri3or  4916  onfr  4923  ordelinel  4982  relin1  5126  resss  5303  resmpt3  5330  cnvcnvss  5467  funin  5661  funimass2  5668  fnresin1  5701  fnres  5703  fresin  5760  fresaun  5762  fresaunres2  5763  nfvres  5902  ssimaex  5939  fneqeql2  5997  funiunfv  6159  isoini2  6234  ofrfval  6543  ofval  6544  ofrval  6545  off  6549  ofres  6550  ofco  6555  fparlem3  6897  fparlem4  6898  smores  7035  smores2  7037  tfrlem5  7061  pmresg  7458  sbthlem7  7645  sbthcl  7651  infi  7755  imafi  7825  ixpfi2  7830  unifpw  7835  f1opwfi  7836  fival  7884  fi0  7892  dffi2  7895  elfiun  7902  dffi3  7903  marypha1lem  7905  ordtypelem3  7957  ordtypelem4  7958  ordtypelem6  7960  ordtypelem7  7961  ordtypelem8  7962  wdomima2g  8024  epfrs  8174  tskwe  8343  r0weon  8402  fodomfi2  8453  infpwfien  8455  ackbij1lem6  8617  ackbij1lem9  8620  ackbij1lem10  8621  ackbij1lem11  8622  ackbij1lem15  8626  ackbij1lem16  8627  fin23lem24  8714  fin23lem26  8717  fin23lem23  8718  fin23lem22  8719  fin23lem19  8728  isfin1-3  8778  ttukeylem6  8906  brdom3  8918  brdom5  8919  brdom4  8920  imadomg  8924  fpwwe2lem12  9031  canthp1lem2  9043  wunin  9103  tskin  9149  gruima  9192  ingru  9205  gruina  9208  grur1a  9209  nqerf  9320  nqerrel  9322  dedekindle  9756  hashun3  12432  hashdif  12456  rexanuz  13157  limsupgle  13279  rlimres  13360  lo1res  13361  lo1resb  13366  rlimresb  13367  o1resb  13368  lo1eq  13370  rlimeq  13371  o1of2  13414  o1rlimmul  13420  isercolllem2  13467  isercolllem3  13468  isercoll  13469  ackbijnn  13619  incexclem  13627  incexc  13628  bitsinvp1  13974  sadcaddlem  13982  sadadd2lem  13984  sadadd3  13986  sadaddlem  13991  sadasslem  13995  sadeq  13997  bitsres  13998  smuval2  14007  smupval  14013  smueqlem  14015  smumul  14018  prmreclem2  14310  ramub2  14407  ramub1lem2  14420  fvsetsid  14531  ressinbas  14567  ressress  14568  submre  14876  submrc  14899  isacs2  14924  isacs1i  14928  mreacs  14929  acsfn  14930  invss  15032  sscres  15069  coffth  15179  catcisolem  15307  catciso  15308  catcoppccl  15309  catcfuccl  15310  catcxpccl  15350  isdrs2  15442  isacs3lem  15669  isacs5lem  15672  acsfiindd  15680  psss  15717  psssdm2  15718  tsrss  15726  tsrdir  15741  resscntz  16240  sylow2a  16510  lsmmod  16564  frgpnabllem2  16749  gsumzres  16785  gsumzresOLD  16789  gsumzaddlem  16805  gsumzaddlemOLD  16807  dprddisj2  16957  dprddisj2OLD  16958  ablfac1eu  16994  ablfac2  17010  isunit  17176  lspextmo  17571  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  23160  xrlimcnp  23162  ppisval  23241  ppifi  23243  ppiprm  23289  ppinprm  23290  chtprm  23291  chtnprm  23292  chtdif  23296  efchtdvds  23297  ppidif  23301  ppiltx  23315  prmorcht  23316  ppiub  23343  chtlepsi  23345  chtleppi  23349  pclogsum  23354  vmasum  23355  chpval2  23357  chpchtsum  23358  chpub  23359  2sqlem8  23511  chebbnd1lem1  23518  chtppilimlem1  23522  rplogsumlem2  23534  rpvmasum2  23561  dchrisum0re  23562  rplogsum  23576  dirith2  23577  axtgcgrrflx  23723  axtgcgrid  23724  axtgsegcon  23725  axtg5seg  23726  axtgbtwnid  23727  axtgpasch  23728  axtgcont1  23729  perpcom  23945  perpneq  23946  ragperp  23949  opidonOLD  25155  flddivrng  25248  phnv  25560  minvecolem2  25622  minvecolem3  25623  minvecolem5  25628  minvecolem6  25629  minvecolem7  25630  hlimcaui  25985  chdmm1i  26226  chabs1  26265  chabs2  26266  ledii  26285  lejdii  26287  pjoml4i  26336  cmbr3i  26349  cmbr4i  26350  cmm1i  26355  osumcor2i  26393  3oalem4  26414  pjssmii  26430  pjocini  26447  pjini  26448  mayete3i  26477  mayete3iOLD  26478  riesz4  26814  riesz1  26815  cnlnadjeui  26827  cnlnadjeu  26828  cnlnssadj  26830  nmopadjlei  26838  pjin1i  26942  pjclem1  26945  stji1i  26992  stm1i  26993  dmdbr2  27053  ssmd1  27061  mdslj2i  27070  mdsl2bi  27073  mdslmd1lem1  27075  mdslmd2i  27080  atomli  27132  atcvat4i  27147  sumdmdlem2  27169  dmdbr5ati  27172  dmdbr6ati  27173  dmdbr7ati  27174  disjin  27277  disjxpin  27278  imadifxp  27289  off2  27312  ffsrn  27383  xrge0tsmsd  27607  ordtrestNEW  27735  qqhnm  27803  qqhcn  27804  rrhre  27831  indf1ofs  27871  esumval  27889  esumel  27890  gsumesum  27899  esumlub  27900  esumcst  27903  esumfsup  27908  esumpcvgval  27916  esumcvg  27924  sigainb  27968  measinb2  28026  sibfinima  28113  sibfof  28114  eulerpartlemelr  28128  eulerpartlem1  28138  eulerpartgbij  28143  eulerpartlemgvv  28147  eulerpartlemgu  28148  eulerpartlemgs2  28151  sseqf  28163  ballotlemfelz  28261  ballotlemfp1  28262  conpcon  28512  iccllyscon  28527  cvmsss2  28551  cvmcov2  28552  cvmopnlem  28555  cvmliftmolem2  28559  cvmliftlem15  28575  cvmlift2lem12  28591  mvrsfpw  28698  msrf  28734  elmsta  28740  mthmpps  28774  nepss  28927  dfon2lem4  29152  predss  29185  wfrlem4  29280  frrlem4  29324  nofulllem5  29400  txpss3v  29462  fixssdm  29490  fixssrn  29491  limitssson  29495  ontopbas  29827  ptrest  29982  mblfinlem3  29987  mblfinlem4  29988  ismblfin  29989  mbfposadd  29996  fneer  30105  neibastop1  30111  neibastop2lem  30112  filnetlem3  30132  sstotbnd2  30204  ssbnd  30218  heibor1lem  30239  heiborlem1  30241  heiborlem3  30243  heiborlem5  30245  heiborlem6  30246  heiborlem10  30250  heibor  30251  exidcl  30272  elrfi  30560  elrfirn  30561  elrfirn2  30562  ismrcd1  30564  istopclsd  30566  isnacs2  30572  mrefg3  30574  isnacs3  30576  diophrw  30626  diophin  30640  aomclem2  30935  islmodfg  30949  lsmfgcl  30954  lmhmfgima  30964  lmhmfgsplit  30966  lmhmlnmsplit  30967  pwfi2f1o  30978  hbt  31013  acsfn1p  31083  islptre  31490  sumnnodd  31501  limclner  31522  cncfuni  31554  fouriersw  31861  fldc  32402  fldhmsubc  32403  onfrALTlem2  32804  onfrALTlem2VD  33175  bnj1292  33359  bj-ablssgrp  34132  lshpinN  34192  lcvexchlem5  34241  pmodlem2  35049  pmod1i  35050  pmodN  35052  osumcllem7N  35164  pexmidlem4N  35175  pl42lem3N  35183  djaclN  36339  dihoml4c  36579  dochdmj1  36593  djhcl  36603  dochexmidlem4  36666  mapd1o  36851  mapdin  36865  taupilemrplb  37172  taupilem2  37174  taupi  37175  fiinfi  37187  xptrrel  37194  trrelind  37197  rp-imass  37205
  Copyright terms: Public domain W3C validator