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

Theorem inss1 3364
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
StepHypRef Expression
1 elin 3333 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 448 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3159 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    i^i cin 3126    C_ wss 3127
This theorem is referenced by:  inss2  3365  ssinss1  3372  unabs  3374  nssinpss  3376  dfin4  3384  inv1  3456  disjdif  3501  uniintsn  3873  epse  4348  wefrc  4359  ordtri3or  4396  onfr  4403  ordelinel  4463  relin1  4791  resss  4967  resmpt3  4989  cnvcnvss  5116  funin  5257  funimass2  5264  fnresin1  5296  fnres  5298  fresin  5348  fresaun  5350  fresaunres2  5351  nfvres  5491  ssimaex  5518  fneqeql2  5568  funiunfv  5708  isoini2  5770  ofrfval  6020  ofval  6021  ofrval  6022  off  6027  ofres  6028  ofco  6031  fparlem3  6154  fparlem4  6155  smores  6337  smores2  6339  pmresg  6763  sbthlem7  6945  sbthcl  6951  imafi  7116  ixpfi2  7122  unifpw  7126  f1opwfi  7127  fival  7134  fi0  7141  dffi2  7144  elfiun  7151  dffi3  7152  marypha1lem  7154  ordtypelem3  7203  ordtypelem4  7204  ordtypelem6  7206  ordtypelem7  7207  ordtypelem8  7208  wdomima2g  7268  epfrs  7381  tskwe  7551  r0weon  7608  fodomfi2  7655  infpwfien  7657  ackbij1lem6  7819  ackbij1lem9  7822  ackbij1lem10  7823  ackbij1lem11  7824  ackbij1lem15  7828  ackbij1lem16  7829  fin23lem24  7916  fin23lem26  7919  fin23lem23  7920  fin23lem22  7921  fin23lem19  7930  isfin1-3  7980  ttukeylem6  8109  brdom3  8121  brdom5  8122  brdom4  8123  imadomg  8127  fpwwe2lem12  8231  canthp1lem2  8243  wunin  8303  tskin  8349  gruima  8392  ingru  8405  gruina  8408  grur1a  8409  nqerf  8522  nqerrel  8524  hashdif  11341  rexanuz  11795  limsupgle  11917  rlimres  11998  lo1res  11999  lo1resb  12004  rlimresb  12005  o1resb  12006  lo1eq  12008  rlimeq  12009  o1of2  12052  o1rlimmul  12058  isercolllem2  12105  isercolllem3  12106  isercoll  12107  ackbijnn  12252  bitsinvp1  12603  sadcaddlem  12611  sadadd2lem  12613  sadadd3  12615  sadaddlem  12620  sadasslem  12624  sadeq  12626  bitsres  12627  smuval2  12636  smupval  12642  smueqlem  12644  smumul  12647  prmreclem2  12927  ramub2  13024  ramub1lem2  13037  ressinbas  13167  ressress  13168  submre  13470  submrc  13493  isacs2  13518  isacs1i  13522  mreacs  13523  acsfn  13524  invss  13626  sscres  13663  coffth  13773  catcisolem  13901  catciso  13902  catcoppccl  13903  catcfuccl  13904  catcxpccl  13944  isdrs2  14036  isacs3lem  14232  isacs5lem  14235  acsfiindd  14243  psss  14286  psssdm2  14287  tsrss  14295  tsrdir  14323  resscntz  14770  sylow2a  14893  lsmmod  14947  frgpnabllem2  15125  gsumzres  15157  gsumzaddlem  15166  dprddisj2  15237  ablfac1eu  15271  ablfac2  15287  isunit  15402  lspextmo  15776  2idlval  15948  aspsubrg  16034  psrbagsn  16199  mplind  16206  zlpirlem2  16405  pjfval  16569  pjpm  16571  basdif0  16654  tgval2  16657  eltg3  16663  unitg  16668  tgcl  16670  tgdom  16679  tgidm  16681  ppttop  16707  epttop  16709  ntropn  16749  ntrin  16761  mretopd  16792  mreclatdemo  16796  restbas  16852  restfpw  16873  restcls  16874  ordtrest  16895  subbascn  16947  cncls  16966  cnpresti  16979  cnprest  16980  fincmp  17083  cmpsublem  17089  cmpsub  17090  fiuncmp  17094  indiscon  17107  connsub  17110  cnconn  17111  iunconlem  17116  clscon  17119  concompclo  17124  islly2  17173  cldllycmp  17184  kgentopon  17196  llycmpkgen2  17208  1stckgenlem  17211  ptbasfi  17239  txcls  17262  txcnp  17277  ptcnplem  17278  txcnmpt  17281  txcmplem2  17299  hausdiag  17302  txkgen  17309  xkopt  17312  xkococnlem  17316  txcon  17346  qtoptop2  17353  basqtop  17365  tgqtop  17366  kqnrmlem1  17397  kqnrmlem2  17398  nrmhmph  17448  fbssfi  17495  filin  17512  infil  17521  fbasrn  17542  fgtr  17548  ufprim  17567  flimrest  17641  hauspwpwf1  17645  txflf  17664  fclsrest  17682  alexsubALTlem3  17706  alexsubALTlem4  17707  ptcmplem5  17713  tsmsres  17789  tsmsxplem1  17798  xmetres  17891  metres  17892  blin2  17938  blbas  17939  blres  17940  setsmstopn  17987  met2ndci  18031  metrest  18033  ressxms  18034  tgioo  18265  xrsmopn  18281  zdis  18285  reconnlem1  18294  reconnlem2  18295  xrge0tsms  18302  cnheibor  18416  lebnum  18425  nmoleub2lem  18558  nmoleub2lem3  18559  nmoleub2lem2  18560  nmoleub3  18563  nmhmcn  18564  tchcph  18630  cfilresi  18684  cfilres  18685  caussi  18686  causs  18687  relcmpcmet  18705  minveclem4a  18757  minveclem4  18759  ismbl2  18849  cmmbl  18855  nulmbl2  18857  unmbl  18858  shftmbl  18859  volinun  18866  voliunlem1  18870  voliunlem2  18871  ioombl1lem4  18881  ioombl1  18882  ioorcl  18895  uniioombllem2  18901  uniioombllem3  18903  uniioombllem4  18904  uniioombllem5  18905  uniioombl  18907  volivth  18925  vitalilem3  18928  vitalilem4  18929  vitalilem5  18930  vitali  18931  mbfadd  18979  mbfsub  18980  i1fima2  18997  i1fd  18999  i1fadd  19013  itg1addlem2  19015  itg1addlem4  19017  itg1addlem5  19018  itg1climres  19032  mbfmul  19044  itg2splitlem  19066  itg2split  19067  limcresi  19198  limciun  19207  limcun  19208  dvreslem  19222  dvres2lem  19223  dvres  19224  dvres3a  19227  dvaddbr  19250  dvmulbr  19251  dvfsumle  19331  dvfsumabs  19333  ig1peu  19520  taylfvallem1  19699  tayl0  19704  pilem2  19791  pilem3  19792  rlimcnp2  20224  xrlimcnp  20226  ppisval  20304  ppifi  20306  ppiprm  20352  ppinprm  20353  chtprm  20354  chtnprm  20355  chtdif  20359  efchtdvds  20360  ppidif  20364  ppiltx  20378  prmorcht  20379  ppiub  20406  chtlepsi  20408  chtleppi  20412  pclogsum  20417  vmasum  20418  chpval2  20420  chpchtsum  20421  chpub  20422  2sqlem8  20574  chebbnd1lem1  20581  chtppilimlem1  20585  rplogsumlem2  20597  rpvmasum2  20624  dchrisum0re  20625  rplogsum  20639  dirith2  20640  opidon  20950  flddivrng  21043  phnv  21353  minvecolem2  21415  minvecolem3  21416  minvecolem5  21421  minvecolem6  21422  minvecolem7  21423  hlimcaui  21777  chdmm1i  22017  chabs1  22056  chabs2  22057  ledii  22076  lejdii  22078  pjoml4i  22127  cmbr3i  22140  cmbr4i  22141  cmm1i  22146  osumcor2i  22184  3oalem4  22205  pjssmii  22221  pjocini  22238  pjini  22239  mayete3i  22268  mayete3iOLD  22269  riesz4  22605  riesz1  22606  cnlnadjeui  22618  cnlnadjeu  22619  cnlnssadj  22621  nmopadjlei  22629  pjin1i  22733  pjclem1  22736  stji1i  22783  stm1i  22784  dmdbr2  22844  ssmd1  22852  mdslj2i  22861  mdsl2bi  22864  mdslmd1lem1  22866  mdslmd2i  22871  atomli  22923  atcvat4i  22938  sumdmdlem2  22960  dmdbr5ati  22963  dmdbr6ati  22964  dmdbr7ati  22965  infi  22990  ballotlemfelz  23011  ballotlemfp1  23012  conpcon  23139  iccllyscon  23154  cvmsss2  23178  cvmcov2  23179  cvmopnlem  23182  cvmliftmolem2  23186  cvmliftlem15  23202  cvmlift2lem12  23218  nepss  23445  dedekindle  23455  dfon2lem4  23512  predss  23543  wfrlem4  23629  frrlem4  23654  txpss3v  23795  fixssdm  23823  fixssrn  23824  ontopbas  24243  domintrefb  24430  posprsr  24608  dfps2  24657  toplat  24658  reacomsmgrp1  24711  reacomsmgrp2  24712  reacomsmgrp3  24713  reacomsmgrp4  24714  clfsebsr  24717  resgcom  24719  clsint  24881  unint2t  24886  limptlimpr2lem2  24943  flfnei2  24945  islimrs4  24950  stfincomp  24959  lvsovso  24994  hdrmp  25074  inttaror  25268  fneer  25656  fnessref  25661  neibastop1  25676  neibastop2lem  25677  filnetlem3  25697  sstotbnd2  25866  ssbnd  25880  heibor1lem  25901  heiborlem1  25903  heiborlem3  25905  heiborlem5  25907  heiborlem6  25908  heiborlem10  25912  heibor  25913  exidcl  25934  elrfi  26137  elrfirn  26138  elrfirn2  26139  ismrcd1  26141  istopclsd  26143  isnacs2  26149  mrefg3  26151  isnacs3  26153  diophrw  26206  diophin  26220  aomclem2  26520  islmodfg  26535  lsmfgcl  26540  lmhmfgima  26550  lmhmfgsplit  26552  lmhmlnmsplit  26553  frlmsplit2  26611  pwfi2f1o  26628  hbt  26702  acsfn1p  26875  onfrALTlem2  27447  onfrALTlem2VD  27798  bnj1292  27980  lshpinN  28429  lcvexchlem5  28478  pmodlem2  29286  pmod1i  29287  pmodN  29289  osumcllem7N  29401  pexmidlem4N  29412  pl42lem3N  29420  djaclN  30576  dihoml4c  30816  dochdmj1  30830  djhcl  30840  dochexmidlem4  30903  mapd1o  31088  mapdin  31102
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator