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

Theorem inss1 3714
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 3683 . . 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 3503 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1819    i^i cin 3470    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485
This theorem is referenced by:  inss2  3715  ssinss1  3722  unabs  3735  nssinpss  3737  dfin4  3745  inv1  3821  disjdif  3903  uniintsn  4326  wefrc  4882  ordtri3or  4919  onfr  4926  ordelinel  4985  relin1  5129  resss  5307  resmpt3  5334  cnvcnvss  5467  funin  5661  funimass2  5668  fnresin1  5701  fnres  5703  fresin  5760  fresaun  5762  fresaunres2  5763  nfvres  5902  ssimaex  5938  fneqeql2  5997  funiunfv  6161  isoini2  6236  ofrfval  6547  ofval  6548  ofrval  6549  off  6553  ofres  6554  ofco  6559  fparlem3  6901  fparlem4  6902  smores  7041  smores2  7043  tfrlem5  7067  pmresg  7465  sbthlem7  7652  sbthcl  7658  infi  7762  imafi  7831  ixpfi2  7836  unifpw  7841  f1opwfi  7842  fival  7890  fi0  7898  dffi2  7901  elfiun  7908  dffi3  7909  marypha1lem  7911  ordtypelem3  7963  ordtypelem4  7964  ordtypelem6  7966  ordtypelem7  7967  ordtypelem8  7968  wdomima2g  8030  epfrs  8179  tskwe  8348  r0weon  8407  fodomfi2  8458  infpwfien  8460  ackbij1lem6  8622  ackbij1lem9  8625  ackbij1lem10  8626  ackbij1lem11  8627  ackbij1lem15  8631  ackbij1lem16  8632  fin23lem24  8719  fin23lem26  8722  fin23lem23  8723  fin23lem22  8724  fin23lem19  8733  isfin1-3  8783  ttukeylem6  8911  brdom3  8923  brdom5  8924  brdom4  8925  imadomg  8929  fpwwe2lem12  9036  canthp1lem2  9048  wunin  9108  tskin  9154  gruima  9197  ingru  9210  gruina  9213  grur1a  9214  nqerf  9325  nqerrel  9327  dedekindle  9762  hashun3  12454  hashdif  12479  rexanuz  13189  limsupgle  13311  rlimres  13392  lo1res  13393  lo1resb  13398  rlimresb  13399  o1resb  13400  lo1eq  13402  rlimeq  13403  o1of2  13446  o1rlimmul  13452  isercolllem2  13499  isercolllem3  13500  isercoll  13501  ackbijnn  13651  incexclem  13659  incexc  13660  bitsinvp1  14110  sadcaddlem  14118  sadadd2lem  14120  sadadd3  14122  sadaddlem  14127  sadasslem  14131  sadeq  14133  bitsres  14134  smuval2  14143  smupval  14149  smueqlem  14151  smumul  14154  prmreclem2  14446  ramub2  14543  ramub1lem2  14556  fvsetsid  14670  ressinbas  14706  ressress  14708  submre  15021  submrc  15044  isacs2  15069  isacs1i  15073  mreacs  15074  acsfn  15075  invss  15176  sscres  15238  coffth  15351  catcisolem  15511  catciso  15512  catcoppccl  15513  catcfuccl  15514  catcxpccl  15602  isdrs2  15694  isacs3lem  15922  isacs5lem  15925  acsfiindd  15933  psss  15970  psssdm2  15971  tsrss  15979  tsrdir  15994  resscntz  16495  sylow2a  16765  lsmmod  16819  frgpnabllem2  17004  gsumzres  17040  gsumzresOLD  17044  gsumzaddlem  17060  gsumzaddlemOLD  17062  dprddisj2  17213  dprddisj2OLD  17214  ablfac1eu  17250  ablfac2  17266  isunit  17432  lspextmo  17828  2idlval  18007  aspsubrg  18106  psrbagsn  18286  mplind  18293  zringlpirlem2  18636  zlpirlem2  18641  pjfval  18863  pjpm  18865  ofco2  19079  basdif0  19580  tgval2  19583  eltg3  19589  unitgOLD  19595  tgcl  19597  tgdom  19606  tgidm  19608  ppttop  19634  epttop  19636  ntropn  19676  ntrin  19688  mretopd  19719  mreclatdemoBAD  19723  neiptoptop  19758  restbas  19785  restfpw  19806  neitr  19807  restcls  19808  ordtrest  19829  subbascn  19881  cncls  19901  cnpresti  19915  cnprest  19916  fincmp  20019  cmpsublem  20025  cmpsub  20026  fiuncmp  20030  indiscon  20044  connsub  20047  cnconn  20048  iunconlem  20053  clscon  20056  concompclo  20061  islly2  20110  cldllycmp  20121  kgentopon  20164  llycmpkgen2  20176  1stckgenlem  20179  ptbasfi  20207  txcls  20230  txcnp  20246  ptcnplem  20247  txcnmpt  20250  txcmplem2  20268  hausdiag  20271  txkgen  20278  xkopt  20281  xkococnlem  20285  txcon  20315  qtoptop2  20325  basqtop  20337  tgqtop  20338  kqnrmlem1  20369  kqnrmlem2  20370  nrmhmph  20420  fbssfi  20463  filin  20480  infil  20489  fbasrn  20510  fgtr  20516  ufprim  20535  flimrest  20609  hauspwpwf1  20613  txflf  20632  fclsrest  20650  alexsubALTlem3  20674  alexsubALTlem4  20675  ptcmplem5  20681  tsmsresOLD  20770  tsmsres  20771  tsmsxplem1  20780  ustund  20849  trust  20857  utoptop  20862  restutop  20865  cfiluweak  20923  xmetres  20992  metres  20993  blin2  21057  blbas  21058  blres  21059  setsmstopn  21106  met2ndci  21150  metrest  21152  ressxms  21153  tgioo  21426  xrsmopn  21442  zdis  21446  reconnlem1  21456  reconnlem2  21457  xrge0tsms  21464  cnheibor  21580  lebnum  21589  nmoleub2lem  21722  nmoleub2lem3  21723  nmoleub2lem2  21724  nmoleub3  21727  nmhmcn  21728  tchcph  21805  cfilresi  21859  cfilres  21860  caussi  21861  causs  21862  relcmpcmet  21880  minveclem4a  21970  minveclem4  21972  ismbl2  22063  cmmbl  22070  nulmbl2  22072  unmbl  22073  shftmbl  22074  volinun  22081  voliunlem1  22085  voliunlem2  22086  ioombl1lem4  22096  ioombl1  22097  ioorcl  22111  uniioombllem2  22117  uniioombllem3  22119  uniioombllem4  22120  uniioombllem5  22121  uniioombl  22123  volivth  22141  vitalilem3  22144  vitalilem4  22145  vitalilem5  22146  vitali  22147  mbfadd  22193  mbfsub  22194  i1fima2  22211  i1fd  22213  i1fadd  22227  itg1addlem2  22229  itg1addlem4  22231  itg1addlem5  22232  itg1climres  22246  mbfmul  22258  itg2splitlem  22280  itg2split  22281  limcresi  22414  limciun  22423  limcun  22424  dvreslem  22438  dvres2lem  22439  dvres  22440  dvres3a  22443  dvaddbr  22466  dvmulbr  22467  dvfsumle  22547  dvfsumabs  22549  ig1peu  22697  taylfvallem1  22877  tayl0  22882  pilem2  22972  pilem3  22973  rlimcnp2  23421  xrlimcnp  23423  ppisval  23502  ppifi  23504  ppiprm  23550  ppinprm  23551  chtprm  23552  chtnprm  23553  chtdif  23557  efchtdvds  23558  ppidif  23562  ppiltx  23576  prmorcht  23577  ppiub  23604  chtlepsi  23606  chtleppi  23610  pclogsum  23615  vmasum  23616  chpval2  23618  chpchtsum  23619  chpub  23620  2sqlem8  23772  chebbnd1lem1  23779  chtppilimlem1  23783  rplogsumlem2  23795  rpvmasum2  23822  dchrisum0re  23823  rplogsum  23837  dirith2  23838  axtgcgrrflx  23984  axtgcgrid  23985  axtgsegcon  23986  axtg5seg  23987  axtgbtwnid  23988  axtgpasch  23989  axtgcont1  23990  perpcom  24215  perpneq  24216  ragperp  24219  opidonOLD  25450  flddivrng  25543  phnv  25855  minvecolem2  25917  minvecolem3  25918  minvecolem5  25923  minvecolem6  25924  minvecolem7  25925  hlimcaui  26280  chdmm1i  26521  chabs1  26560  chabs2  26561  ledii  26580  lejdii  26582  pjoml4i  26631  cmbr3i  26644  cmbr4i  26645  cmm1i  26650  osumcor2i  26688  3oalem4  26709  pjssmii  26725  pjocini  26742  pjini  26743  mayete3i  26772  mayete3iOLD  26773  riesz4  27109  riesz1  27110  cnlnadjeui  27122  cnlnadjeu  27123  cnlnssadj  27125  nmopadjlei  27133  pjin1i  27237  pjclem1  27240  stji1i  27287  stm1i  27288  dmdbr2  27348  ssmd1  27356  mdslj2i  27365  mdsl2bi  27368  mdslmd1lem1  27370  mdslmd2i  27375  atomli  27427  atcvat4i  27442  sumdmdlem2  27464  dmdbr5ati  27467  dmdbr6ati  27468  dmdbr7ati  27469  disjin  27583  disjxpin  27584  imadifxp  27595  off2  27624  ffsrn  27702  xrge0tsmsd  27928  ordtrestNEW  28056  qqhnm  28124  qqhcn  28125  rrhre  28152  indf1ofs  28192  esumval  28212  esumel  28213  gsumesum  28222  esumlub  28223  esumcst  28226  esumfsup  28232  esumpcvgval  28240  esumcvg  28248  sigainb  28297  measinb2  28355  sibfinima  28456  sibfof  28457  eulerpartlemelr  28471  eulerpartlem1  28481  eulerpartgbij  28486  eulerpartlemgvv  28490  eulerpartlemgu  28491  eulerpartlemgs2  28494  sseqf  28506  ballotlemfelz  28604  ballotlemfp1  28605  conpcon  28855  iccllyscon  28870  cvmsss2  28894  cvmcov2  28895  cvmopnlem  28898  cvmliftmolem2  28902  cvmliftlem15  28918  cvmlift2lem12  28934  mvrsfpw  29041  msrf  29077  elmsta  29083  mthmpps  29117  nepss  29270  dfon2lem4  29392  predss  29425  wfrlem4  29520  frrlem4  29564  nofulllem5  29640  txpss3v  29690  fixssdm  29718  fixssrn  29719  limitssson  29723  ontopbas  30055  ptrest  30210  mblfinlem3  30215  mblfinlem4  30216  ismblfin  30217  mbfposadd  30224  fneer  30333  neibastop1  30339  neibastop2lem  30340  filnetlem3  30360  sstotbnd2  30432  ssbnd  30446  heibor1lem  30467  heiborlem1  30469  heiborlem3  30471  heiborlem5  30473  heiborlem6  30474  heiborlem10  30478  heibor  30479  exidcl  30500  elrfi  30788  elrfirn  30789  elrfirn2  30790  ismrcd1  30792  istopclsd  30794  isnacs2  30800  mrefg3  30802  isnacs3  30804  diophrw  30854  diophin  30868  aomclem2  31163  islmodfg  31177  lsmfgcl  31182  lmhmfgima  31192  lmhmfgsplit  31194  lmhmlnmsplit  31195  pwfi2f1o  31206  hbt  31241  acsfn1p  31310  islptre  31786  sumnnodd  31797  limclner  31818  cncfuni  31850  fouriersw  32175  rngcbas  32875  rngchomfval  32876  rngccofval  32880  dfrngc2  32882  rnghmsscmap2  32883  rnghmsscmap  32884  rngcsect  32890  funcrngcsetc  32908  ringcbas  32921  ringchomfval  32922  ringccofval  32926  dfringc2  32928  rhmsscmap2  32929  rhmsscmap  32930  rhmsscrnghm  32936  ringcsect  32941  funcringcsetc  32945  funcringcsetcOLD2lem9  32954  fldc  32993  fldhmsubc  32994  rngcrescrhm  32995  rhmsubclem1  32996  fldcOLD  33012  fldhmsubcOLD  33013  rngcrescrhmOLD  33014  rhmsubcOLDlem1  33015  onfrALTlem2  33419  onfrALTlem2VD  33790  bnj1292  33975  bj-ablssgrp  34755  lshpinN  34815  lcvexchlem5  34864  pmodlem2  35672  pmod1i  35673  pmodN  35675  osumcllem7N  35787  pexmidlem4N  35798  pl42lem3N  35806  djaclN  36964  dihoml4c  37204  dochdmj1  37218  djhcl  37228  dochexmidlem4  37291  mapd1o  37476  mapdin  37490  taupilemrplb  37796  taupilem2  37798  taupi  37799  fiinfi  37859  xptrrel  37876  trrelind  37879  rp-imass  37896
  Copyright terms: Public domain W3C validator