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

Theorem inss1 3331
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 3300 . . 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 3126 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    i^i cin 3093    C_ wss 3094
This theorem is referenced by:  inss2  3332  ssinss1  3339  unabs  3341  nssinpss  3343  dfin4  3351  inv1  3423  disjdif  3468  uniintsn  3840  epse  4313  wefrc  4324  ordtri3or  4361  onfr  4368  ordelinel  4428  relin1  4756  resss  4932  resmpt3  4954  cnvcnvss  5081  funin  5222  funimass2  5229  fnresin1  5261  fnres  5263  fresin  5313  fresaun  5315  fresaunres2  5316  nfvres  5456  ssimaex  5483  fneqeql2  5533  funiunfv  5673  isoini2  5735  ofrfval  5985  ofval  5986  ofrval  5987  off  5992  ofres  5993  ofco  5996  fparlem3  6119  fparlem4  6120  smores  6302  smores2  6304  pmresg  6728  sbthlem7  6910  sbthcl  6916  imafi  7081  ixpfi2  7087  unifpw  7091  f1opwfi  7092  fival  7099  fi0  7106  dffi2  7109  elfiun  7116  dffi3  7117  marypha1lem  7119  ordtypelem3  7168  ordtypelem4  7169  ordtypelem6  7171  ordtypelem7  7172  ordtypelem8  7173  wdomima2g  7233  epfrs  7346  tskwe  7516  r0weon  7573  fodomfi2  7620  infpwfien  7622  ackbij1lem6  7784  ackbij1lem9  7787  ackbij1lem10  7788  ackbij1lem11  7789  ackbij1lem15  7793  ackbij1lem16  7794  fin23lem24  7881  fin23lem26  7884  fin23lem23  7885  fin23lem22  7886  fin23lem19  7895  isfin1-3  7945  ttukeylem6  8074  brdom3  8086  brdom5  8087  brdom4  8088  imadomg  8092  fpwwe2lem12  8196  canthp1lem2  8208  wunin  8268  tskin  8314  gruima  8357  ingru  8370  gruina  8373  grur1a  8374  nqerf  8487  nqerrel  8489  hashdif  11305  rexanuz  11759  limsupgle  11881  rlimres  11962  lo1res  11963  lo1resb  11968  rlimresb  11969  o1resb  11970  lo1eq  11972  rlimeq  11973  o1of2  12016  o1rlimmul  12022  isercolllem2  12069  isercolllem3  12070  isercoll  12071  ackbijnn  12216  bitsinvp1  12567  sadcaddlem  12575  sadadd2lem  12577  sadadd3  12579  sadaddlem  12584  sadasslem  12588  sadeq  12590  bitsres  12591  smuval2  12600  smupval  12606  smueqlem  12608  smumul  12611  prmreclem2  12891  ramub2  12988  ramub1lem2  13001  ressinbas  13131  ressress  13132  submre  13434  submrc  13457  isacs2  13482  isacs1i  13486  mreacs  13487  acsfn  13488  invss  13590  sscres  13627  coffth  13737  catcisolem  13865  catciso  13866  catcoppccl  13867  catcfuccl  13868  catcxpccl  13908  isdrs2  14000  isacs3lem  14196  isacs5lem  14199  acsfiindd  14207  psss  14250  psssdm2  14251  tsrss  14259  tsrdir  14287  resscntz  14734  sylow2a  14857  lsmmod  14911  frgpnabllem2  15089  gsumzres  15121  gsumzaddlem  15130  dprddisj2  15201  ablfac1eu  15235  ablfac2  15251  isunit  15366  lspextmo  15740  2idlval  15912  aspsubrg  15998  psrbagsn  16163  mplind  16170  zlpirlem2  16369  pjfval  16533  pjpm  16535  basdif0  16618  tgval2  16621  eltg3  16627  unitg  16632  tgcl  16634  tgdom  16643  tgidm  16645  ppttop  16671  epttop  16673  ntropn  16713  ntrin  16725  mretopd  16756  mreclatdemo  16760  restbas  16816  restfpw  16837  restcls  16838  ordtrest  16859  subbascn  16911  cncls  16930  cnpresti  16943  cnprest  16944  fincmp  17047  cmpsublem  17053  cmpsub  17054  fiuncmp  17058  indiscon  17071  connsub  17074  cnconn  17075  iunconlem  17080  clscon  17083  concompclo  17088  islly2  17137  cldllycmp  17148  kgentopon  17160  llycmpkgen2  17172  1stckgenlem  17175  ptbasfi  17203  txcls  17226  txcnp  17241  ptcnplem  17242  txcnmpt  17245  txcmplem2  17263  hausdiag  17266  txkgen  17273  xkopt  17276  xkococnlem  17280  txcon  17310  qtoptop2  17317  basqtop  17329  tgqtop  17330  kqnrmlem1  17361  kqnrmlem2  17362  nrmhmph  17412  fbssfi  17459  filin  17476  infil  17485  fbasrn  17506  fgtr  17512  ufprim  17531  flimrest  17605  hauspwpwf1  17609  txflf  17628  fclsrest  17646  alexsubALTlem3  17670  alexsubALTlem4  17671  ptcmplem5  17677  tsmsres  17753  tsmsxplem1  17762  xmetres  17855  metres  17856  blin2  17902  blbas  17903  blres  17904  setsmstopn  17951  met2ndci  17995  metrest  17997  ressxms  17998  tgioo  18229  xrsmopn  18245  zdis  18249  reconnlem1  18258  reconnlem2  18259  xrge0tsms  18266  cnheibor  18380  lebnum  18389  nmoleub2lem  18522  nmoleub2lem3  18523  nmoleub2lem2  18524  nmoleub3  18527  nmhmcn  18528  tchcph  18594  cfilresi  18648  cfilres  18649  caussi  18650  causs  18651  relcmpcmet  18669  minveclem4a  18721  minveclem4  18723  ismbl2  18813  cmmbl  18819  nulmbl2  18821  unmbl  18822  shftmbl  18823  volinun  18830  voliunlem1  18834  voliunlem2  18835  ioombl1lem4  18845  ioombl1  18846  ioorcl  18859  uniioombllem2  18865  uniioombllem3  18867  uniioombllem4  18868  uniioombllem5  18869  uniioombl  18871  volivth  18889  vitalilem3  18892  vitalilem4  18893  vitalilem5  18894  vitali  18895  mbfadd  18943  mbfsub  18944  i1fima2  18961  i1fd  18963  i1fadd  18977  itg1addlem2  18979  itg1addlem4  18981  itg1addlem5  18982  itg1climres  18996  mbfmul  19008  itg2splitlem  19030  itg2split  19031  limcresi  19162  limciun  19171  limcun  19172  dvreslem  19186  dvres2lem  19187  dvres  19188  dvres3a  19191  dvaddbr  19214  dvmulbr  19215  dvfsumle  19295  dvfsumabs  19297  ig1peu  19484  taylfvallem1  19663  tayl0  19668  pilem2  19755  pilem3  19756  rlimcnp2  20188  xrlimcnp  20190  ppisval  20268  ppifi  20270  ppiprm  20316  ppinprm  20317  chtprm  20318  chtnprm  20319  chtdif  20323  efchtdvds  20324  ppidif  20328  ppiltx  20342  prmorcht  20343  ppiub  20370  chtlepsi  20372  chtleppi  20376  pclogsum  20381  vmasum  20382  chpval2  20384  chpchtsum  20385  chpub  20386  2sqlem8  20538  chebbnd1lem1  20545  chtppilimlem1  20549  rplogsumlem2  20561  rpvmasum2  20588  dchrisum0re  20589  rplogsum  20603  dirith2  20604  opidon  20914  flddivrng  21007  phnv  21317  minvecolem2  21379  minvecolem3  21380  minvecolem5  21385  minvecolem6  21386  minvecolem7  21387  hlimcaui  21741  chdmm1i  21981  chabs1  22020  chabs2  22021  ledii  22040  lejdii  22042  pjoml4i  22109  cmbr3i  22122  cmbr4i  22123  cmm1i  22128  osumcor2i  22166  3oalem4  22187  pjssmii  22203  pjocini  22220  pjini  22221  mayete3i  22250  mayete3iOLD  22251  riesz4  22569  riesz1  22570  cnlnadjeui  22582  cnlnadjeu  22583  cnlnssadj  22585  nmopadjlei  22593  pjin1i  22697  pjclem1  22700  stji1i  22747  stm1i  22748  dmdbr2  22808  ssmd1  22816  mdslj2i  22825  mdsl2bi  22828  mdslmd1lem1  22830  mdslmd2i  22835  atomli  22887  atcvat4i  22902  sumdmdlem2  22924  dmdbr5ati  22927  dmdbr6ati  22928  dmdbr7ati  22929  infi  22954  ballotlemfelz  22975  ballotlemfp1  22976  conpcon  23103  iccllyscon  23118  cvmsss2  23142  cvmcov2  23143  cvmopnlem  23146  cvmliftmolem2  23150  cvmliftlem15  23166  cvmlift2lem12  23182  nepss  23409  dedekindle  23419  dfon2lem4  23476  predss  23507  wfrlem4  23593  frrlem4  23618  txpss3v  23759  fixssdm  23787  fixssrn  23788  ontopbas  24207  domintrefb  24394  posprsr  24572  dfps2  24621  toplat  24622  reacomsmgrp1  24675  reacomsmgrp2  24676  reacomsmgrp3  24677  reacomsmgrp4  24678  clfsebsr  24681  resgcom  24683  clsint  24845  unint2t  24850  limptlimpr2lem2  24907  flfnei2  24909  islimrs4  24914  stfincomp  24923  lvsovso  24958  hdrmp  25038  inttaror  25232  fneer  25620  fnessref  25625  neibastop1  25640  neibastop2lem  25641  filnetlem3  25661  sstotbnd2  25830  ssbnd  25844  heibor1lem  25865  heiborlem1  25867  heiborlem3  25869  heiborlem5  25871  heiborlem6  25872  heiborlem10  25876  heibor  25877  exidcl  25898  elrfi  26101  elrfirn  26102  elrfirn2  26103  ismrcd1  26105  istopclsd  26107  isnacs2  26113  mrefg3  26115  isnacs3  26117  diophrw  26170  diophin  26184  aomclem2  26484  islmodfg  26499  lsmfgcl  26504  lmhmfgima  26514  lmhmfgsplit  26516  lmhmlnmsplit  26517  frlmsplit2  26575  pwfi2f1o  26592  hbt  26666  acsfn1p  26839  onfrALTlem2  27327  onfrALTlem2VD  27678  bnj1292  27860  lshpinN  28309  lcvexchlem5  28358  pmodlem2  29166  pmod1i  29167  pmodN  29169  osumcllem7N  29281  pexmidlem4N  29292  pl42lem3N  29300  djaclN  30456  dihoml4c  30696  dochdmj1  30710  djhcl  30720  dochexmidlem4  30783  mapd1o  30968  mapdin  30982
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator