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

Theorem inss2 3351
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 3322 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3350 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3170 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3112    C_ wss 3113
This theorem is referenced by:  difin0  3488  ordin  4380  onfr  4389  ordelinel  4449  relin2  4778  relres  4957  ssrnres  5090  cnvcnv  5100  fnresin2  5283  fresaunres2  5337  ssimaex  5504  exfo  5598  ffvresb  5610  ofrfval  6006  ofval  6007  ofrval  6008  offres  6012  off  6013  ofres  6014  ofco  6017  fnwelem  6150  fnse  6152  tpostpos  6174  smores3  6324  erinxp  6687  pmresg  6749  nnfi  7007  ixpfi2  7108  f1opwfi  7113  dffi2  7130  elfiun  7137  marypha1lem  7140  ordtypelem3  7189  ordtypelem6  7192  ordtypelem7  7193  hartogslem1  7211  unxpwdom  7257  epfrs  7367  tcmin  7380  bnd2  7517  tskwe  7537  r0weon  7594  infxpenlem  7595  fodomfi2  7641  infpwfien  7643  cdainf  7772  ackbij1lem6  7805  ackbij1lem9  7808  ackbij1lem10  7809  ackbij1lem11  7810  ackbij1lem15  7814  ackbij1lem16  7815  ackbij1lem18  7817  ackbij1b  7819  sdom2en01  7882  fin23lem26  7905  fin23lem13  7912  isfin1-3  7966  fin56  7973  fin1a2lem9  7988  ttukeylem6  8095  brdom3  8107  brdom5  8108  brdom4  8109  fpwwe2lem8  8213  fpwwe2lem9  8214  fpwwe2lem12  8217  fpwwe2  8219  canthwelem  8226  gruima  8378  ingru  8391  gruina  8394  grur1a  8395  ltrelpi  8467  ltrelnq  8504  nqerf  8508  fzfi  10986  rexanuz  11780  limsupgord  11897  limsupcl  11898  limsupgf  11900  limsupgle  11902  rlimres  11983  lo1res  11984  o1of2  12037  o1rlimmul  12043  ackbijnn  12237  bitsinv1  12581  bitsinvp1  12588  sadcaddlem  12596  sadadd2lem  12598  sadadd3  12600  sadaddlem  12605  sadasslem  12609  sadeq  12611  smuval2  12621  smupval  12627  smueqlem  12629  prmrec  12917  isstruct2  13105  structcnvcnv  13107  ressbasss  13148  ressress  13153  restsspw  13284  pwsle  13339  submre  13455  isacs2  13503  isacs1i  13507  sscres  13648  rescabs  13658  resscat  13674  funcres2c  13723  coffth  13758  rescfth  13759  ressffth  13760  catccatid  13882  catcisolem  13886  catciso  13887  catcoppccl  13888  catcfuccl  13889  catcxpccl  13929  yoniso  14007  isdrs2  14021  isacs3lem  14217  acsinfd  14231  acsdomd  14232  psssdm2  14272  tsrss  14280  sylow2a  14878  lsmmod  14932  frgpnabllem2  15110  subrgpropd  15527  lssacs  15672  sralmod  15887  asplss  16017  ressmplbas  16148  subrgmpl  16152  opsrtoslem2  16174  mplind  16191  ressply1bas  16255  zlpirlem2  16390  zlpirlem3  16391  basdif0  16639  eltg4i  16646  ntrss2  16742  ntrin  16746  isopn3  16751  mreclatdemo  16781  restbas  16837  resttopon  16840  restuni2  16846  restcld  16851  restfpw  16858  ordtrest  16880  subbascn  16932  cnrest2r  16963  cnpresti  16964  cnprest  16965  lmss  16974  cnrmi  17036  restcnrm  17038  resthauslem  17039  fincmp  17068  imacmp  17072  fiuncmp  17079  cmpfi  17083  cnconn  17096  iuncon  17102  clscon  17104  concompclo  17109  1stcrest  17127  subislly  17155  islly2  17158  cldllycmp  17169  hauspwdom  17175  kgeni  17180  llycmpkgen2  17193  1stckgenlem  17196  ptbasfi  17224  txcls  17247  ptclsg  17257  txcnp  17262  ptcnplem  17263  txtube  17282  txcmplem1  17283  txcmplem2  17284  txkgen  17294  xkopt  17297  xkococnlem  17301  txcon  17331  basqtop  17350  tgqtop  17351  kqdisj  17371  kqnrmlem1  17382  kqnrmlem2  17383  nrmhmph  17433  infil  17506  fbasrn  17527  trfg  17534  uzrest  17540  isufil2  17551  fmfnfmlem4  17600  hauspwpwf1  17630  txflf  17649  alexsubALTlem3  17691  alexsubALTlem4  17692  ptcmplem2  17695  tmdgsum2  17727  tsmsres  17774  tsmsxplem1  17783  blres  17925  met2ndci  18016  metrest  18018  tgioo  18250  zdis  18270  reconnlem2  18280  reconn  18281  cnheibor  18401  lebnum  18410  nmoleub2lem3  18544  nmoleub3  18548  cphsqrcl  18568  tchcph  18615  cfilresi  18669  cfilres  18670  caussi  18671  causs  18672  minveclem4b  18743  minveclem4  18744  ovolfcl  18774  ovolfioo  18775  ovolficc  18776  ovolficcss  18777  ovolfsval  18778  ovolfsf  18779  ovollb  18786  ovoliunlem1  18809  ovolicc2lem1  18824  ovolicc2lem2  18825  ovolicc2lem3  18826  ovolicc2lem4  18827  ovolicc2lem5  18828  ovolicc2  18829  nulmbl  18841  voliunlem1  18855  ioombl1lem4  18866  ovolfs2  18874  uniiccdif  18881  uniioovol  18882  uniiccvol  18883  uniioombllem2a  18885  uniioombllem2  18886  uniioombllem3a  18887  uniioombllem3  18888  uniioombllem4  18889  uniioombllem5  18890  uniioombllem6  18891  uniioombl  18892  dyadmbllem  18902  dyadmbl  18903  opnmbllem  18904  volcn  18909  volivth  18910  vitalilem2  18912  vitalilem4  18914  mbfadd  18964  mbfsub  18965  i1fima  18981  i1fima2  18982  i1fd  18984  i1fadd  18998  i1fmul  18999  itg1addlem2  19000  itg1addlem4  19002  itg1addlem5  19003  i1fres  19008  mbfmul  19029  itg2cnlem2  19065  bddmulibl  19141  ellimc2  19175  ellimc3  19177  limcflf  19179  limcresi  19183  limciun  19192  dvreslem  19207  dvres2lem  19208  dvres3a  19212  cpnres  19234  dvaddbr  19235  dvmulbr  19236  dvmptres3  19253  lhop1lem  19308  pf1rcl  19380  ig1peu  19505  taylfvallem1  19684  tayl0  19689  rlimcnp2  20209  xrlimcnp  20211  ppisval  20289  chtf  20294  efchtcl  20297  chtge0  20298  ppinprm  20338  chtprm  20339  chtnprm  20340  chtwordi  20342  chtdif  20344  efchtdvds  20345  chtlepsi  20393  chtleppi  20397  pclogsum  20402  chpval2  20405  chpchtsum  20406  chpub  20407  2sqlem8  20559  2sqlem9  20560  chebbnd1lem1  20566  chtppilimlem1  20570  rplogsumlem2  20582  rpvmasumlem  20584  rplogsum  20624  dirith2  20625  issubgo  20916  opidon  20935  chdmm1i  22002  chm0i  22015  ledii  22061  lejdii  22063  pjoml2i  22128  pjoml4i  22130  cmcmlem  22134  cmbr4i  22144  osumcori  22186  pjssmii  22224  mayete3i  22271  mayete3iOLD  22272  riesz4  22590  riesz1  22591  cnlnadjeu  22604  nmopadjlei  22614  pjclem1  22721  pjci  22726  mdbr3  22823  mdbr4  22824  dmdbr2  22829  dmdbr5  22834  ssmd2  22838  mdslj1i  22845  mdslj2i  22846  mdsl1i  22847  mdsl2bi  22849  mdslmd1lem1  22851  mdslmd1lem2  22852  mdslmd2i  22856  csmdsymi  22860  cvexchlem  22894  atomli  22908  atcvat4i  22923  conpcon  23124  iccllyscon  23139  cvmsss2  23163  cvmcov2  23164  cvmopnlem  23167  cvmliftmolem2  23171  cvmlift2lem12  23203  nepss  23430  dedekindle  23440  dfon2lem4  23497  wfrlem4  23614  frrlem4  23639  domintrefb  24415  toplat  24643  reacomsmgrp1  24696  reacomsmgrp2  24697  reacomsmgrp3  24698  limptlimpr2lem2  24928  lvsovso  24979  tartarmap  25241  inttarcar  25254  cardtar  25257  bsstrs  25499  nbssntrs  25500  trer  25580  neiin  25603  neibastop1  25661  neibastop2lem  25662  topmeet  25666  filnetlem3  25682  heibor1lem  25886  heiborlem1  25888  heiborlem3  25890  heiborlem10  25897  elrfi  26122  elrfirn  26123  fnwe2lem2  26501  aomclem2  26505  lsmfgcl  26525  lmhmfgima  26535  lmhmfgsplit  26537  lmhmlnmsplit  26538  uvcff  26593  hbt  26687  mvdco  26741  acsfn1p  26860  onfrALTlem3  27346  onfrALTlem2  27348  onfrALTlem3VD  27697  onfrALTlem2VD  27699  bnj1293  27882  lshpinN  28330  lcvexchlem1  28375  lcvexchlem5  28379  pmod1i  29188  pmodN  29190  osumcllem7N  29302  pexmidlem4N  29313  dochdmj1  30731  dochexmidlem4  30804  lcfrlem25  30908  mapd1o  30989  mapdin  31003
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 2759  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator