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

Theorem inss2 3297
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
inss2  |-  ( A  i^i  B )  C_  B

Proof of Theorem inss2
StepHypRef Expression
1 incom 3269 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3296 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3130 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3077    C_ wss 3078
This theorem is referenced by:  difin0  3433  ordin  4315  onfr  4324  relin2  4711  relres  4890  ssrnres  5023  cnvcnv  5033  fnresin2  5216  fresaunres2  5270  ssimaex  5436  exfo  5530  ffvresb  5542  ofrfval  5938  ofval  5939  ofrval  5940  offres  5944  off  5945  ofres  5946  ofco  5949  fnwelem  6082  fnse  6084  tpostpos  6106  smores3  6256  erinxp  6619  pmresg  6681  nnfi  6938  ixpfi2  7038  f1opwfi  7043  dffi2  7060  elfiun  7067  marypha1lem  7070  ordtypelem3  7119  ordtypelem6  7122  ordtypelem7  7123  hartogslem1  7141  unxpwdom  7187  epfrs  7297  tcmin  7310  bnd2  7447  tskwe  7467  r0weon  7524  infxpenlem  7525  fodomfi2  7571  infpwfien  7573  cdainf  7702  ackbij1lem6  7735  ackbij1lem9  7738  ackbij1lem10  7739  ackbij1lem11  7740  ackbij1lem15  7744  ackbij1lem16  7745  ackbij1lem18  7747  ackbij1b  7749  sdom2en01  7812  fin23lem26  7835  fin23lem13  7842  isfin1-3  7896  fin56  7903  fin1a2lem9  7918  ttukeylem6  8025  brdom3  8037  brdom5  8038  brdom4  8039  fpwwe2lem8  8139  fpwwe2lem9  8140  fpwwe2lem12  8143  fpwwe2  8145  canthwelem  8152  gruima  8304  ingru  8317  gruina  8320  grur1a  8321  ltrelpi  8393  ltrelnq  8430  nqerf  8434  fzfi  10912  rexanuz  11706  limsupgord  11823  limsupcl  11824  limsupgf  11826  limsupgle  11828  rlimres  11909  lo1res  11910  o1of2  11963  o1rlimmul  11969  ackbijnn  12163  bitsinv1  12507  bitsinvp1  12514  sadcaddlem  12522  sadadd2lem  12524  sadadd3  12526  sadaddlem  12531  sadasslem  12535  sadeq  12537  smuval2  12547  smupval  12553  smueqlem  12555  prmrec  12843  isstruct2  13031  structcnvcnv  13033  ressbasss  13074  ressress  13079  restsspw  13210  pwsle  13265  submre  13379  isacs2  13400  isacs1i  13403  sscres  13544  rescabs  13554  resscat  13570  funcres2c  13619  coffth  13654  rescfth  13655  ressffth  13656  catccatid  13778  catcisolem  13782  catciso  13783  catcoppccl  13784  catcfuccl  13785  catcxpccl  13825  yoniso  13903  isdrs2  13917  isacs3lem  14113  psssdm2  14159  tsrss  14167  sylow2a  14765  lsmmod  14819  frgpnabllem2  14997  subrgpropd  15414  lssacs  15559  sralmod  15771  asplss  15901  ressmplbas  16032  subrgmpl  16036  opsrtoslem2  16058  mplind  16075  ressply1bas  16139  zlpirlem2  16274  zlpirlem3  16275  basdif0  16523  eltg4i  16530  ntrss2  16626  ntrin  16630  isopn3  16635  mreclatdemo  16665  restbas  16721  resttopon  16724  restuni2  16730  restcld  16735  restfpw  16742  ordtrest  16764  subbascn  16816  cnrest2r  16847  cnpresti  16848  cnprest  16849  lmss  16858  cnrmi  16920  restcnrm  16922  resthauslem  16923  fincmp  16952  imacmp  16956  fiuncmp  16963  cmpfi  16967  cnconn  16980  iuncon  16986  clscon  16988  concompclo  16993  1stcrest  17011  subislly  17039  islly2  17042  cldllycmp  17053  hauspwdom  17059  kgeni  17064  llycmpkgen2  17077  1stckgenlem  17080  ptbasfi  17108  txcls  17131  ptclsg  17141  txcnp  17146  ptcnplem  17147  txtube  17166  txcmplem1  17167  txcmplem2  17168  txkgen  17178  xkopt  17181  xkococnlem  17185  txcon  17215  basqtop  17234  tgqtop  17235  kqdisj  17255  kqnrmlem1  17266  kqnrmlem2  17267  nrmhmph  17317  infil  17390  fbasrn  17411  trfg  17418  uzrest  17424  isufil2  17435  fmfnfmlem4  17484  hauspwpwf1  17514  txflf  17533  alexsubALTlem3  17575  alexsubALTlem4  17576  ptcmplem2  17579  tmdgsum2  17611  tsmsres  17658  tsmsxplem1  17667  blres  17809  met2ndci  17900  metrest  17902  tgioo  18134  zdis  18154  reconnlem2  18164  reconn  18165  cnheibor  18285  lebnum  18294  nmoleub2lem3  18428  nmoleub3  18432  cphsqrcl  18452  tchcph  18499  cfilresi  18553  cfilres  18554  caussi  18555  causs  18556  minveclem4b  18627  minveclem4  18628  ovolfcl  18658  ovolfioo  18659  ovolficc  18660  ovolficcss  18661  ovolfsval  18662  ovolfsf  18663  ovollb  18670  ovoliunlem1  18693  ovolicc2lem1  18708  ovolicc2lem2  18709  ovolicc2lem3  18710  ovolicc2lem4  18711  ovolicc2lem5  18712  ovolicc2  18713  nulmbl  18725  voliunlem1  18739  ioombl1lem4  18750  ovolfs2  18758  uniiccdif  18765  uniioovol  18766  uniiccvol  18767  uniioombllem2a  18769  uniioombllem2  18770  uniioombllem3a  18771  uniioombllem3  18772  uniioombllem4  18773  uniioombllem5  18774  uniioombllem6  18775  uniioombl  18776  dyadmbllem  18786  dyadmbl  18787  opnmbllem  18788  volcn  18793  volivth  18794  vitalilem2  18796  vitalilem4  18798  mbfadd  18848  mbfsub  18849  i1fima  18865  i1fima2  18866  i1fd  18868  i1fadd  18882  i1fmul  18883  itg1addlem2  18884  itg1addlem4  18886  itg1addlem5  18887  i1fres  18892  mbfmul  18913  itg2cnlem2  18949  bddmulibl  19025  ellimc2  19059  ellimc3  19061  limcflf  19063  limcresi  19067  limciun  19076  dvreslem  19091  dvres2lem  19092  dvres3a  19096  cpnres  19118  dvaddbr  19119  dvmulbr  19120  dvmptres3  19137  lhop1lem  19192  pf1rcl  19264  ig1peu  19389  taylfvallem1  19568  tayl0  19573  rlimcnp2  20093  xrlimcnp  20095  ppisval  20173  chtf  20178  efchtcl  20181  chtge0  20182  ppinprm  20222  chtprm  20223  chtnprm  20224  chtwordi  20226  chtdif  20228  efchtdvds  20229  chtlepsi  20277  chtleppi  20281  pclogsum  20286  chpval2  20289  chpchtsum  20290  chpub  20291  2sqlem8  20443  2sqlem9  20444  chebbnd1lem1  20450  chtppilimlem1  20454  rplogsumlem2  20466  rpvmasumlem  20468  rplogsum  20508  dirith2  20509  issubgo  20800  opidon  20819  chdmm1i  21886  chm0i  21899  ledii  21945  lejdii  21947  pjoml2i  22012  pjoml4i  22014  cmcmlem  22018  cmbr4i  22028  osumcori  22070  pjssmii  22108  mayete3i  22155  mayete3iOLD  22156  riesz4  22474  riesz1  22475  cnlnadjeu  22488  nmopadjlei  22498  pjclem1  22605  pjci  22610  mdbr3  22707  mdbr4  22708  dmdbr2  22713  dmdbr5  22718  ssmd2  22722  mdslj1i  22729  mdslj2i  22730  mdsl1i  22731  mdsl2bi  22733  mdslmd1lem1  22735  mdslmd1lem2  22736  mdslmd2i  22740  csmdsymi  22744  cvexchlem  22778  atomli  22792  atcvat4i  22807  conpcon  22937  iccllyscon  22952  cvmsss2  22976  cvmcov2  22977  cvmopnlem  22980  cvmliftmolem2  22984  cvmlift2lem12  23016  nepss  23243  dedekindle  23253  dfon2lem4  23310  wfrlem4  23427  frrlem4  23452  domintrefb  24228  toplat  24456  reacomsmgrp1  24509  reacomsmgrp2  24510  reacomsmgrp3  24511  limptlimpr2lem2  24741  lvsovso  24792  tartarmap  25054  inttarcar  25067  cardtar  25070  bsstrs  25312  nbssntrs  25313  trer  25393  neiin  25416  neibastop1  25474  neibastop2lem  25475  topmeet  25479  filnetlem3  25495  heibor1lem  25699  heiborlem1  25701  heiborlem3  25703  heiborlem10  25710  elrfi  25935  elrfirn  25936  fnwe2lem2  26314  aomclem2  26318  lsmfgcl  26338  lmhmfgima  26348  lmhmfgsplit  26350  lmhmlnmsplit  26351  uvcff  26406  hbt  26500  mvdco  26554  acsfn1p  26673  onfrALTlem3  27099  onfrALTlem2  27101  onfrALTlem3VD  27450  onfrALTlem2VD  27452  bnj1293  27635  lshpinN  28083  lcvexchlem1  28128  lcvexchlem5  28132  pmod1i  28941  pmodN  28943  osumcllem7N  29055  pexmidlem4N  29066  dochdmj1  30484  dochexmidlem4  30557  lcfrlem25  30661  mapd1o  30742  mapdin  30756
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator