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

Theorem inss1 3389
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 3358 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 446 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3184 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1684    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  inss2  3390  ssinss1  3397  unabs  3399  nssinpss  3401  dfin4  3409  inv1  3481  disjdif  3526  uniintsn  3899  epse  4376  wefrc  4387  ordtri3or  4424  onfr  4431  ordelinel  4491  relin1  4803  resss  4979  resmpt3  5001  cnvcnvss  5128  funin  5319  funimass2  5326  fnresin1  5358  fnres  5360  fresin  5410  fresaun  5412  fresaunres2  5413  nfvres  5557  ssimaex  5584  fneqeql2  5634  funiunfv  5774  isoini2  5836  ofrfval  6086  ofval  6087  ofrval  6088  off  6093  ofres  6094  ofco  6097  fparlem3  6220  fparlem4  6221  smores  6369  smores2  6371  pmresg  6795  sbthlem7  6977  sbthcl  6983  imafi  7148  ixpfi2  7154  unifpw  7158  f1opwfi  7159  fival  7166  fi0  7173  dffi2  7176  elfiun  7183  dffi3  7184  marypha1lem  7186  ordtypelem3  7235  ordtypelem4  7236  ordtypelem6  7238  ordtypelem7  7239  ordtypelem8  7240  wdomima2g  7300  epfrs  7413  tskwe  7583  r0weon  7640  fodomfi2  7687  infpwfien  7689  ackbij1lem6  7851  ackbij1lem9  7854  ackbij1lem10  7855  ackbij1lem11  7856  ackbij1lem15  7860  ackbij1lem16  7861  fin23lem24  7948  fin23lem26  7951  fin23lem23  7952  fin23lem22  7953  fin23lem19  7962  isfin1-3  8012  ttukeylem6  8141  brdom3  8153  brdom5  8154  brdom4  8155  imadomg  8159  fpwwe2lem12  8263  canthp1lem2  8275  wunin  8335  tskin  8381  gruima  8424  ingru  8437  gruina  8440  grur1a  8441  nqerf  8554  nqerrel  8556  hashun3  11366  hashdif  11375  rexanuz  11829  limsupgle  11951  rlimres  12032  lo1res  12033  lo1resb  12038  rlimresb  12039  o1resb  12040  lo1eq  12042  rlimeq  12043  o1of2  12086  o1rlimmul  12092  isercolllem2  12139  isercolllem3  12140  isercoll  12141  ackbijnn  12286  incexclem  12295  incexc  12296  bitsinvp1  12640  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  bitsres  12664  smuval2  12673  smupval  12679  smueqlem  12681  smumul  12684  prmreclem2  12964  ramub2  13061  ramub1lem2  13074  ressinbas  13204  ressress  13205  submre  13507  submrc  13530  isacs2  13555  isacs1i  13559  mreacs  13560  acsfn  13561  invss  13663  sscres  13700  coffth  13810  catcisolem  13938  catciso  13939  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  isdrs2  14073  isacs3lem  14269  isacs5lem  14272  acsfiindd  14280  psss  14323  psssdm2  14324  tsrss  14332  tsrdir  14360  resscntz  14807  sylow2a  14930  lsmmod  14984  frgpnabllem2  15162  gsumzres  15194  gsumzaddlem  15203  dprddisj2  15274  ablfac1eu  15308  ablfac2  15324  isunit  15439  lspextmo  15813  2idlval  15985  aspsubrg  16071  psrbagsn  16236  mplind  16243  zlpirlem2  16442  pjfval  16606  pjpm  16608  basdif0  16691  tgval2  16694  eltg3  16700  unitg  16705  tgcl  16707  tgdom  16716  tgidm  16718  ppttop  16744  epttop  16746  ntropn  16786  ntrin  16798  mretopd  16829  mreclatdemo  16833  restbas  16889  restfpw  16910  restcls  16911  ordtrest  16932  subbascn  16984  cncls  17003  cnpresti  17016  cnprest  17017  fincmp  17120  cmpsublem  17126  cmpsub  17127  fiuncmp  17131  indiscon  17144  connsub  17147  cnconn  17148  iunconlem  17153  clscon  17156  concompclo  17161  islly2  17210  cldllycmp  17221  kgentopon  17233  llycmpkgen2  17245  1stckgenlem  17248  ptbasfi  17276  txcls  17299  txcnp  17314  ptcnplem  17315  txcnmpt  17318  txcmplem2  17336  hausdiag  17339  txkgen  17346  xkopt  17349  xkococnlem  17353  txcon  17383  qtoptop2  17390  basqtop  17402  tgqtop  17403  kqnrmlem1  17434  kqnrmlem2  17435  nrmhmph  17485  fbssfi  17532  filin  17549  infil  17558  fbasrn  17579  fgtr  17585  ufprim  17604  flimrest  17678  hauspwpwf1  17682  txflf  17701  fclsrest  17719  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem5  17750  tsmsres  17826  tsmsxplem1  17835  xmetres  17928  metres  17929  blin2  17975  blbas  17976  blres  17977  setsmstopn  18024  met2ndci  18068  metrest  18070  ressxms  18071  tgioo  18302  xrsmopn  18318  zdis  18322  reconnlem1  18331  reconnlem2  18332  xrge0tsms  18339  cnheibor  18453  lebnum  18462  nmoleub2lem  18595  nmoleub2lem3  18596  nmoleub2lem2  18597  nmoleub3  18600  nmhmcn  18601  tchcph  18667  cfilresi  18721  cfilres  18722  caussi  18723  causs  18724  relcmpcmet  18742  minveclem4a  18794  minveclem4  18796  ismbl2  18886  cmmbl  18892  nulmbl2  18894  unmbl  18895  shftmbl  18896  volinun  18903  voliunlem1  18907  voliunlem2  18908  ioombl1lem4  18918  ioombl1  18919  ioorcl  18932  uniioombllem2  18938  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  volivth  18962  vitalilem3  18965  vitalilem4  18966  vitalilem5  18967  vitali  18968  mbfadd  19016  mbfsub  19017  i1fima2  19034  i1fd  19036  i1fadd  19050  itg1addlem2  19052  itg1addlem4  19054  itg1addlem5  19055  itg1climres  19069  mbfmul  19081  itg2splitlem  19103  itg2split  19104  limcresi  19235  limciun  19244  limcun  19245  dvreslem  19259  dvres2lem  19260  dvres  19261  dvres3a  19264  dvaddbr  19287  dvmulbr  19288  dvfsumle  19368  dvfsumabs  19370  ig1peu  19557  taylfvallem1  19736  tayl0  19741  pilem2  19828  pilem3  19829  rlimcnp2  20261  xrlimcnp  20263  ppisval  20341  ppifi  20343  ppiprm  20389  ppinprm  20390  chtprm  20391  chtnprm  20392  chtdif  20396  efchtdvds  20397  ppidif  20401  ppiltx  20415  prmorcht  20416  ppiub  20443  chtlepsi  20445  chtleppi  20449  pclogsum  20454  vmasum  20455  chpval2  20457  chpchtsum  20458  chpub  20459  2sqlem8  20611  chebbnd1lem1  20618  chtppilimlem1  20622  rplogsumlem2  20634  rpvmasum2  20661  dchrisum0re  20662  rplogsum  20676  dirith2  20677  opidon  20989  flddivrng  21082  phnv  21392  minvecolem2  21454  minvecolem3  21455  minvecolem5  21460  minvecolem6  21461  minvecolem7  21462  hlimcaui  21816  chdmm1i  22056  chabs1  22095  chabs2  22096  ledii  22115  lejdii  22117  pjoml4i  22166  cmbr3i  22179  cmbr4i  22180  cmm1i  22185  osumcor2i  22223  3oalem4  22244  pjssmii  22260  pjocini  22277  pjini  22278  mayete3i  22307  mayete3iOLD  22308  riesz4  22644  riesz1  22645  cnlnadjeui  22657  cnlnadjeu  22658  cnlnssadj  22660  nmopadjlei  22668  pjin1i  22772  pjclem1  22775  stji1i  22822  stm1i  22823  dmdbr2  22883  ssmd1  22891  mdslj2i  22900  mdsl2bi  22903  mdslmd1lem1  22905  mdslmd2i  22910  atomli  22962  atcvat4i  22977  sumdmdlem2  22999  dmdbr5ati  23002  dmdbr6ati  23003  dmdbr7ati  23004  infi  23029  ballotlemfelz  23049  ballotlemfp1  23050  infi1  23169  off2  23208  disjin  23362  xrge0tsmsd  23382  esumval  23425  esumel  23426  esumcst  23436  esumpcvgval  23446  esumcvg  23454  sigainb  23497  measinb2  23550  indf1ofs  23609  conpcon  23766  iccllyscon  23781  cvmsss2  23805  cvmcov2  23806  cvmopnlem  23809  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift2lem12  23845  nepss  24072  dedekindle  24083  dfon2lem4  24142  predss  24173  wfrlem4  24259  frrlem4  24284  nofulllem5  24360  txpss3v  24418  fixssdm  24446  fixssrn  24447  ontopbas  24867  domintrefb  25063  posprsr  25240  dfps2  25289  toplat  25290  reacomsmgrp1  25343  reacomsmgrp2  25344  reacomsmgrp3  25345  reacomsmgrp4  25346  clfsebsr  25349  resgcom  25351  clsint  25513  unint2t  25518  limptlimpr2lem2  25575  flfnei2  25577  islimrs4  25582  stfincomp  25591  lvsovso  25626  hdrmp  25706  inttaror  25900  fneer  26288  fnessref  26293  neibastop1  26308  neibastop2lem  26309  filnetlem3  26329  sstotbnd2  26498  ssbnd  26512  heibor1lem  26533  heiborlem1  26535  heiborlem3  26537  heiborlem5  26539  heiborlem6  26540  heiborlem10  26544  heibor  26545  exidcl  26566  elrfi  26769  elrfirn  26770  elrfirn2  26771  ismrcd1  26773  istopclsd  26775  isnacs2  26781  mrefg3  26783  isnacs3  26785  diophrw  26838  diophin  26852  aomclem2  27152  islmodfg  27167  lsmfgcl  27172  lmhmfgima  27182  lmhmfgsplit  27184  lmhmlnmsplit  27185  frlmsplit2  27243  pwfi2f1o  27260  hbt  27334  acsfn1p  27507  onfrALTlem2  28311  onfrALTlem2VD  28665  bnj1292  28848  lshpinN  29179  lcvexchlem5  29228  pmodlem2  30036  pmod1i  30037  pmodN  30039  osumcllem7N  30151  pexmidlem4N  30162  pl42lem3N  30170  djaclN  31326  dihoml4c  31566  dochdmj1  31580  djhcl  31590  dochexmidlem4  31653  mapd1o  31838  mapdin  31852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator