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

Theorem inss1 3643
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 3608 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 467 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3422 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1904    i^i cin 3389    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404
This theorem is referenced by:  inss2  3644  ssinss1  3651  unabs  3664  nssinpss  3666  dfin4  3674  inv1  3764  disjdif  3830  uniintsn  4263  wefrc  4833  relin1  4956  resss  5134  resmpt3  5161  cnvcnvss  5297  predss  5394  ordtri3or  5462  onfr  5469  ordelinel  5528  funin  5660  funimass2  5667  fnresin1  5700  fnres  5702  fresin  5764  fresaun  5766  fresaunres2  5767  nfvres  5909  ssimaex  5945  fneqeql2  6006  funiunfv  6171  isoini2  6248  ofrfval  6558  ofval  6559  ofrval  6560  off  6565  ofres  6566  ofco  6570  fparlem3  6917  fparlem4  6918  wfrlem4  7057  smores  7089  smores2  7091  tfrlem5  7116  pmresg  7517  sbthlem7  7706  sbthcl  7712  infi  7813  imafi  7885  ixpfi2  7890  unifpw  7895  f1opwfi  7896  fival  7944  fi0  7952  dffi2  7955  elfiun  7962  dffi3  7963  marypha1lem  7965  ordtypelem3  8053  ordtypelem4  8054  ordtypelem6  8056  ordtypelem7  8057  ordtypelem8  8058  wdomima2g  8119  epfrs  8233  tskwe  8402  r0weon  8461  fodomfi2  8509  infpwfien  8511  ackbij1lem6  8673  ackbij1lem9  8676  ackbij1lem10  8677  ackbij1lem11  8678  ackbij1lem15  8682  ackbij1lem16  8683  fin23lem24  8770  fin23lem26  8773  fin23lem23  8774  fin23lem22  8775  fin23lem19  8784  isfin1-3  8834  ttukeylem6  8962  brdom3  8974  brdom5  8975  brdom4  8976  imadomg  8980  fpwwe2lem12  9084  canthp1lem2  9096  wunin  9156  tskin  9202  gruima  9245  ingru  9258  gruina  9261  grur1a  9262  nqerf  9373  nqerrel  9375  dedekindle  9816  hashun3  12601  hashin  12626  hashdif  12628  xptrrel  13119  rexanuz  13485  limsupgle  13612  rlimres  13699  lo1res  13700  lo1resb  13705  rlimresb  13706  o1resb  13707  lo1eq  13709  rlimeq  13710  o1of2  13753  o1rlimmul  13759  isercolllem2  13806  isercolllem3  13807  isercoll  13808  ackbijnn  13963  incexclem  13971  incexc  13972  bitsinvp1  14502  sadcaddlem  14510  sadadd2lem  14512  sadadd3  14514  sadaddlem  14519  sadasslem  14523  sadeq  14525  bitsres  14526  smuval2  14535  smupval  14541  smueqlem  14543  smumul  14546  prmreclem2  14940  ramub2  15050  ramub1lem2  15064  fvsetsid  15226  ressinbas  15263  ressress  15265  submre  15589  submrc  15612  isacs2  15637  isacs1i  15641  mreacs  15642  acsfn  15643  invss  15744  sscres  15806  coffth  15919  catcisolem  16079  catciso  16080  catcoppccl  16081  catcfuccl  16082  catcxpccl  16170  isdrs2  16262  isacs3lem  16490  isacs5lem  16493  acsfiindd  16501  psss  16538  psssdm2  16539  tsrss  16547  tsrdir  16562  resscntz  17063  sylow2a  17349  lsmmod  17403  frgpnabllem2  17588  gsumzres  17621  gsumzaddlem  17632  dprddisj2  17750  ablfac1eu  17784  ablfac2  17800  isunit  17963  lspextmo  18357  2idlval  18534  aspsubrg  18632  psrbagsn  18795  mplind  18802  zringlpirlem2OLD  19131  zringlpirlem2  19133  pjfval  19346  pjpm  19348  ofco2  19553  basdif0  20045  tgval2  20048  eltg3  20054  unitgOLD  20060  tgcl  20062  tgdom  20071  tgidm  20073  ppttop  20099  epttop  20101  ntropn  20141  ntrin  20153  mretopd  20185  mreclatdemoBAD  20189  neiptoptop  20224  restbas  20251  restfpw  20272  neitr  20273  restcls  20274  ordtrest  20295  subbascn  20347  cncls  20367  cnpresti  20381  cnprest  20382  fincmp  20485  cmpsublem  20491  cmpsub  20492  fiuncmp  20496  indiscon  20510  connsub  20513  cnconn  20514  iunconlem  20519  clscon  20522  concompclo  20527  islly2  20576  cldllycmp  20587  kgentopon  20630  llycmpkgen2  20642  1stckgenlem  20645  ptbasfi  20673  txcls  20696  txcnp  20712  ptcnplem  20713  txcnmpt  20716  txcmplem2  20734  hausdiag  20737  txkgen  20744  xkopt  20747  xkococnlem  20751  txcon  20781  qtoptop2  20791  basqtop  20803  tgqtop  20804  kqnrmlem1  20835  kqnrmlem2  20836  nrmhmph  20886  fbssfi  20930  filin  20947  infil  20956  fbasrn  20977  fgtr  20983  ufprim  21002  flimrest  21076  hauspwpwf1  21080  txflf  21099  fclsrest  21117  alexsubALTlem3  21142  alexsubALTlem4  21143  ptcmplem5  21149  tsmsres  21236  tsmsxplem1  21245  ustund  21314  trust  21322  utoptop  21327  restutop  21330  cfiluweak  21388  xmetres  21457  metres  21458  blin2  21522  blbas  21523  blres  21524  setsmstopn  21571  met2ndci  21615  metrest  21617  ressxms  21618  tgioo  21892  xrsmopn  21908  zdis  21912  reconnlem1  21922  reconnlem2  21923  xrge0tsms  21930  cnheibor  22061  lebnum  22073  nmoleub2lem  22206  nmoleub2lem3  22207  nmoleub2lem2  22208  nmoleub3  22211  nmhmcn  22212  tchcph  22289  cfilresi  22343  cfilres  22344  caussi  22345  causs  22346  relcmpcmet  22364  minveclem4a  22450  minveclem4  22452  minveclem4aOLD  22462  minveclem4OLD  22464  ismbl2  22559  cmmbl  22566  nulmbl2  22568  unmbl  22569  shftmbl  22570  volinun  22578  voliunlem1  22582  voliunlem2  22583  ioombl1lem4  22593  ioombl1  22594  ioorcl  22608  ioorclOLD  22613  uniioombllem2  22619  uniioombllem2OLD  22620  uniioombllem3  22622  uniioombllem4  22623  uniioombllem5  22624  uniioombl  22626  volivth  22644  vitalilem3  22647  vitalilem4  22648  vitalilem5  22649  vitali  22650  mbfadd  22696  mbfsub  22697  i1fima2  22716  i1fd  22718  i1fadd  22732  itg1addlem2  22734  itg1addlem4  22736  itg1addlem5  22737  itg1climres  22751  mbfmul  22763  itg2splitlem  22785  itg2split  22786  limcresi  22919  limciun  22928  limcun  22929  dvreslem  22943  dvres2lem  22944  dvres  22945  dvres3a  22948  dvaddbr  22971  dvmulbr  22972  dvfsumle  23052  dvfsumabs  23054  ig1peu  23201  ig1peuOLD  23202  taylfvallem1  23391  tayl0  23396  pilem2  23486  pilem2OLD  23487  pilem3  23488  pilem3OLD  23489  rlimcnp2  23971  xrlimcnp  23973  ppisval  24109  ppifi  24111  ppiprm  24157  ppinprm  24158  chtprm  24159  chtnprm  24160  chtdif  24164  efchtdvds  24165  ppidif  24169  ppiltx  24183  prmorcht  24184  ppiub  24211  chtlepsi  24213  chtleppi  24217  pclogsum  24222  vmasum  24223  chpval2  24225  chpchtsum  24226  chpub  24227  2sqlem8  24379  chebbnd1lem1  24386  chtppilimlem1  24390  rplogsumlem2  24402  rpvmasum2  24429  dchrisum0re  24430  rplogsum  24444  dirith2  24445  axtgcgrrflx  24589  axtgcgrid  24590  axtgsegcon  24591  axtg5seg  24592  axtgbtwnid  24593  axtgpasch  24594  axtgcont1  24595  perpcom  24837  perpneq  24838  ragperp  24841  opidonOLD  26131  flddivrng  26224  phnv  26536  minvecolem2  26598  minvecolem3  26599  minvecolem5  26604  minvecolem6  26605  minvecolem7  26606  minvecolem2OLD  26608  minvecolem3OLD  26609  minvecolem5OLD  26614  minvecolem6OLD  26615  minvecolem7OLD  26616  hlimcaui  26970  chdmm1i  27211  chabs1  27250  chabs2  27251  ledii  27270  lejdii  27272  pjoml4i  27321  cmbr3i  27334  cmbr4i  27335  cmm1i  27340  osumcor2i  27378  3oalem4  27399  pjssmii  27415  pjocini  27432  pjini  27433  mayete3i  27462  riesz4  27798  riesz1  27799  cnlnadjeui  27811  cnlnadjeu  27812  cnlnssadj  27814  nmopadjlei  27822  pjin1i  27926  pjclem1  27929  stji1i  27976  stm1i  27977  dmdbr2  28037  ssmd1  28045  mdslj2i  28054  mdsl2bi  28057  mdslmd1lem1  28059  mdslmd2i  28064  atomli  28116  atcvat4i  28131  sumdmdlem2  28153  dmdbr5ati  28156  dmdbr6ati  28157  dmdbr7ati  28158  disjin  28273  disjxpin  28275  imadifxp  28288  off2  28318  ffsrn  28389  gsummptres  28621  xrge0tsmsd  28622  ordtrestNEW  28801  qqhnm  28868  qqhcn  28869  rrhre  28899  indf1ofs  28921  esumval  28941  esumel  28942  gsumesum  28954  esumlub  28955  esumcst  28958  esumfsup  28965  esumpcvgval  28973  esumcvg  28981  sigainb  29032  ldgenpisyslem1  29059  measinb2  29119  sibfinima  29245  sibfof  29246  eulerpartlemelr  29263  eulerpartlem1  29273  eulerpartgbij  29278  eulerpartlemgvv  29282  eulerpartlemgu  29283  eulerpartlemgs2  29286  sseqf  29298  ballotlemfelz  29396  ballotlemfp1  29397  bnj1292  29699  conpcon  30030  iccllyscon  30045  cvmsss2  30069  cvmcov2  30070  cvmopnlem  30073  cvmliftmolem2  30077  cvmliftlem15  30093  cvmlift2lem12  30109  mvrsfpw  30216  msrf  30252  elmsta  30258  mthmpps  30292  nepss  30422  dfon2lem4  30503  frrlem4  30588  nofulllem5  30666  txpss3v  30716  fixssdm  30744  fixssrn  30745  limitssson  30749  fneer  31080  neibastop1  31086  neibastop2lem  31087  filnetlem3  31107  ontopbas  31159  bj-ablssgrp  31763  taupilemrplb  31791  taupilem2  31793  taupi  31794  ptrest  32003  poimirlem29  32033  mblfinlem3  32043  mblfinlem4  32044  ismblfin  32045  mbfposadd  32052  sstotbnd2  32170  ssbnd  32184  heibor1lem  32205  heiborlem1  32207  heiborlem3  32209  heiborlem5  32211  heiborlem6  32212  heiborlem10  32216  heibor  32217  exidcl  32238  lshpinN  32626  lcvexchlem5  32675  pmodlem2  33483  pmod1i  33484  pmodN  33486  osumcllem7N  33598  pexmidlem4N  33609  pl42lem3N  33617  djaclN  34775  dihoml4c  35015  dochdmj1  35029  djhcl  35039  dochexmidlem4  35102  mapd1o  35287  mapdin  35301  elrfi  35607  elrfirn  35608  elrfirn2  35609  ismrcd1  35611  istopclsd  35613  isnacs2  35619  mrefg3  35621  isnacs3  35623  diophrw  35672  diophin  35686  aomclem2  35984  islmodfg  35998  lsmfgcl  36003  lmhmfgima  36013  lmhmfgsplit  36015  lmhmlnmsplit  36016  pwfi2f1o  36025  hbt  36060  acsfn1p  36136  elinintrab  36254  trrelind  36328  rp-imass  36437  onfrALTlem2  36982  onfrALTlem2VD  37349  inmap  37562  fsumiunss  37750  islptre  37796  sumnnodd  37807  limclner  37829  cncfuni  37861  ismbl3  37961  ismbl4  37968  fouriersw  38207  qndenserrnbllem  38275  salincl  38296  salgencntex  38314  sge0less  38348  sge0resplit  38362  sge0split  38365  sge0iunmptlemre  38371  carageniuncllem1  38461  carageniuncllem2  38462  caragenel2d  38472  hspmbllem3  38568  hspmbl  38569  ovolval2lem  38583  rngcbas  40475  rngchomfval  40476  rngccofval  40480  dfrngc2  40482  rnghmsscmap2  40483  rnghmsscmap  40484  rngcsect  40490  funcrngcsetc  40508  ringcbas  40521  ringchomfval  40522  ringccofval  40526  dfringc2  40528  rhmsscmap2  40529  rhmsscmap  40530  rhmsscrnghm  40536  ringcsect  40541  funcringcsetc  40545  funcringcsetcALTV2lem9  40554  fldc  40593  fldhmsubc  40594  rngcrescrhm  40595  rhmsubclem1  40596  fldcALTV  40612  fldhmsubcALTV  40613  rngcrescrhmALTV  40614  rhmsubcALTVlem1  40615
  Copyright terms: Public domain W3C validator