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

Theorem inss1 3554
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 3523 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 447 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3345 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    i^i cin 3312    C_ wss 3313
This theorem is referenced by:  inss2  3555  ssinss1  3562  unabs  3564  nssinpss  3566  dfin4  3574  inv1  3647  disjdif  3693  uniintsn  4080  wefrc  4569  ordtri3or  4606  onfr  4613  ordelinel  4673  relin1  4985  resss  5163  resmpt3  5185  cnvcnvss  5318  funin  5513  funimass2  5520  fnresin1  5552  fnres  5554  fresin  5605  fresaun  5607  fresaunres2  5608  nfvres  5753  ssimaex  5781  fneqeql2  5832  funiunfv  5988  isoini2  6052  ofrfval  6306  ofval  6307  ofrval  6308  off  6313  ofres  6314  ofco  6317  fparlem3  6441  fparlem4  6442  smores  6607  smores2  6609  pmresg  7034  sbthlem7  7216  sbthcl  7222  infi  7325  imafi  7392  ixpfi2  7398  unifpw  7402  f1opwfi  7403  fival  7410  fi0  7418  dffi2  7421  elfiun  7428  dffi3  7429  marypha1lem  7431  ordtypelem3  7482  ordtypelem4  7483  ordtypelem6  7485  ordtypelem7  7486  ordtypelem8  7487  wdomima2g  7547  epfrs  7660  tskwe  7830  r0weon  7887  fodomfi2  7934  infpwfien  7936  ackbij1lem6  8098  ackbij1lem9  8101  ackbij1lem10  8102  ackbij1lem11  8103  ackbij1lem15  8107  ackbij1lem16  8108  fin23lem24  8195  fin23lem26  8198  fin23lem23  8199  fin23lem22  8200  fin23lem19  8209  isfin1-3  8259  ttukeylem6  8387  brdom3  8399  brdom5  8400  brdom4  8401  imadomg  8405  fpwwe2lem12  8509  canthp1lem2  8521  wunin  8581  tskin  8627  gruima  8670  ingru  8683  gruina  8686  grur1a  8687  nqerf  8800  nqerrel  8802  hashun3  11651  hashdif  11671  rexanuz  12142  limsupgle  12264  rlimres  12345  lo1res  12346  lo1resb  12351  rlimresb  12352  o1resb  12353  lo1eq  12355  rlimeq  12356  o1of2  12399  o1rlimmul  12405  isercolllem2  12452  isercolllem3  12453  isercoll  12454  ackbijnn  12600  incexclem  12609  incexc  12610  bitsinvp1  12954  sadcaddlem  12962  sadadd2lem  12964  sadadd3  12966  sadaddlem  12971  sadasslem  12975  sadeq  12977  bitsres  12978  smuval2  12987  smupval  12993  smueqlem  12995  smumul  12998  prmreclem2  13278  ramub2  13375  ramub1lem2  13388  ressinbas  13518  ressress  13519  submre  13823  submrc  13846  isacs2  13871  isacs1i  13875  mreacs  13876  acsfn  13877  invss  13979  sscres  14016  coffth  14126  catcisolem  14254  catciso  14255  catcoppccl  14256  catcfuccl  14257  catcxpccl  14297  isdrs2  14389  isacs3lem  14585  isacs5lem  14588  acsfiindd  14596  psss  14639  psssdm2  14640  tsrss  14648  tsrdir  14676  resscntz  15123  sylow2a  15246  lsmmod  15300  frgpnabllem2  15478  gsumzres  15510  gsumzaddlem  15519  dprddisj2  15590  ablfac1eu  15624  ablfac2  15640  isunit  15755  lspextmo  16125  2idlval  16297  aspsubrg  16383  psrbagsn  16548  mplind  16555  zlpirlem2  16762  pjfval  16926  pjpm  16928  basdif0  17011  tgval2  17014  eltg3  17020  unitg  17025  tgcl  17027  tgdom  17036  tgidm  17038  ppttop  17064  epttop  17066  ntropn  17106  ntrin  17118  mretopd  17149  mreclatdemo  17153  neiptoptop  17188  restbas  17215  restfpw  17236  neitr  17237  restcls  17238  ordtrest  17259  subbascn  17311  cncls  17331  cnpresti  17345  cnprest  17346  fincmp  17449  cmpsublem  17455  cmpsub  17456  fiuncmp  17460  indiscon  17474  connsub  17477  cnconn  17478  iunconlem  17483  clscon  17486  concompclo  17491  islly2  17540  cldllycmp  17551  kgentopon  17563  llycmpkgen2  17575  1stckgenlem  17578  ptbasfi  17606  txcls  17629  txcnp  17645  ptcnplem  17646  txcnmpt  17649  txcmplem2  17667  hausdiag  17670  txkgen  17677  xkopt  17680  xkococnlem  17684  txcon  17714  qtoptop2  17724  basqtop  17736  tgqtop  17737  kqnrmlem1  17768  kqnrmlem2  17769  nrmhmph  17819  fbssfi  17862  filin  17879  infil  17888  fbasrn  17909  fgtr  17915  ufprim  17934  flimrest  18008  hauspwpwf1  18012  txflf  18031  fclsrest  18049  alexsubALTlem3  18073  alexsubALTlem4  18074  ptcmplem5  18080  tsmsres  18166  tsmsxplem1  18175  ustund  18244  trust  18252  utoptop  18257  restutop  18260  cfiluweak  18318  xmetres  18387  metres  18388  blin2  18452  blbas  18453  blres  18454  setsmstopn  18501  met2ndci  18545  metrest  18547  ressxms  18548  tgioo  18820  xrsmopn  18836  zdis  18840  reconnlem1  18850  reconnlem2  18851  xrge0tsms  18858  cnheibor  18973  lebnum  18982  nmoleub2lem  19115  nmoleub2lem3  19116  nmoleub2lem2  19117  nmoleub3  19120  nmhmcn  19121  tchcph  19187  cfilresi  19241  cfilres  19242  caussi  19243  causs  19244  relcmpcmet  19262  minveclem4a  19324  minveclem4  19326  ismbl2  19416  cmmbl  19422  nulmbl2  19424  unmbl  19425  shftmbl  19426  volinun  19433  voliunlem1  19437  voliunlem2  19438  ioombl1lem4  19448  ioombl1  19449  ioorcl  19462  uniioombllem2  19468  uniioombllem3  19470  uniioombllem4  19471  uniioombllem5  19472  uniioombl  19474  volivth  19492  vitalilem3  19495  vitalilem4  19496  vitalilem5  19497  vitali  19498  mbfadd  19546  mbfsub  19547  i1fima2  19564  i1fd  19566  i1fadd  19580  itg1addlem2  19582  itg1addlem4  19584  itg1addlem5  19585  itg1climres  19599  mbfmul  19611  itg2splitlem  19633  itg2split  19634  limcresi  19765  limciun  19774  limcun  19775  dvreslem  19789  dvres2lem  19790  dvres  19791  dvres3a  19794  dvaddbr  19817  dvmulbr  19818  dvfsumle  19898  dvfsumabs  19900  ig1peu  20087  taylfvallem1  20266  tayl0  20271  pilem2  20361  pilem3  20362  rlimcnp2  20798  xrlimcnp  20800  ppisval  20879  ppifi  20881  ppiprm  20927  ppinprm  20928  chtprm  20929  chtnprm  20930  chtdif  20934  efchtdvds  20935  ppidif  20939  ppiltx  20953  prmorcht  20954  ppiub  20981  chtlepsi  20983  chtleppi  20987  pclogsum  20992  vmasum  20993  chpval2  20995  chpchtsum  20996  chpub  20997  2sqlem8  21149  chebbnd1lem1  21156  chtppilimlem1  21160  rplogsumlem2  21172  rpvmasum2  21199  dchrisum0re  21200  rplogsum  21214  dirith2  21215  opidon  21903  flddivrng  21996  phnv  22308  minvecolem2  22370  minvecolem3  22371  minvecolem5  22376  minvecolem6  22377  minvecolem7  22378  hlimcaui  22732  chdmm1i  22972  chabs1  23011  chabs2  23012  ledii  23031  lejdii  23033  pjoml4i  23082  cmbr3i  23095  cmbr4i  23096  cmm1i  23101  osumcor2i  23139  3oalem4  23160  pjssmii  23176  pjocini  23193  pjini  23194  mayete3i  23223  mayete3iOLD  23224  riesz4  23560  riesz1  23561  cnlnadjeui  23573  cnlnadjeu  23574  cnlnssadj  23576  nmopadjlei  23584  pjin1i  23688  pjclem1  23691  stji1i  23738  stm1i  23739  dmdbr2  23799  ssmd1  23807  mdslj2i  23816  mdsl2bi  23819  mdslmd1lem1  23821  mdslmd2i  23826  atomli  23878  atcvat4i  23893  sumdmdlem2  23915  dmdbr5ati  23918  dmdbr6ati  23919  dmdbr7ati  23920  disjin  24020  disjxpin  24021  imadifxp  24031  off2  24047  xrge0tsmsd  24216  qqhnm  24367  qqhcn  24368  rrhre  24380  indf1ofs  24416  esumval  24434  esumel  24435  gsumesum  24444  esumlub  24445  esumcst  24448  esumfsup  24453  esumpcvgval  24461  esumcvg  24469  sigainb  24512  measunl  24563  measinb2  24570  sibfof  24647  ballotlemfelz  24741  ballotlemfp1  24742  conpcon  24915  iccllyscon  24930  cvmsss2  24954  cvmcov2  24955  cvmopnlem  24958  cvmliftmolem2  24962  cvmliftlem15  24978  cvmlift2lem12  24994  nepss  25168  dedekindle  25181  dfon2lem4  25406  predss  25439  wfrlem4  25534  frrlem4  25578  nofulllem5  25654  txpss3v  25716  fixssdm  25744  fixssrn  25745  limitssson  25749  ontopbas  26171  mblfinlem2  26236  mblfinlem3  26237  ismblfin  26238  mbfposadd  26245  fneer  26360  fnessref  26365  neibastop1  26380  neibastop2lem  26381  filnetlem3  26401  sstotbnd2  26475  ssbnd  26489  heibor1lem  26510  heiborlem1  26512  heiborlem3  26514  heiborlem5  26516  heiborlem6  26517  heiborlem10  26521  heibor  26522  exidcl  26543  elrfi  26740  elrfirn  26741  elrfirn2  26742  ismrcd1  26744  istopclsd  26746  isnacs2  26752  mrefg3  26754  isnacs3  26756  diophrw  26809  diophin  26823  aomclem2  27122  islmodfg  27136  lsmfgcl  27141  lmhmfgima  27151  lmhmfgsplit  27153  lmhmlnmsplit  27154  frlmsplit2  27212  pwfi2f1o  27229  hbt  27303  acsfn1p  27476  onfrALTlem2  28570  onfrALTlem2VD  28939  bnj1292  29125  lshpinN  29725  lcvexchlem5  29774  pmodlem2  30582  pmod1i  30583  pmodN  30585  osumcllem7N  30697  pexmidlem4N  30708  pl42lem3N  30716  djaclN  31872  dihoml4c  32112  dochdmj1  32126  djhcl  32136  dochexmidlem4  32199  mapd1o  32384  mapdin  32398
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-in 3320  df-ss 3327
  Copyright terms: Public domain W3C validator