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

Theorem inss2 3564
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 3535 . 2  |-  ( B  i^i  A )  =  ( A  i^i  B
)
2 inss1 3563 . 2  |-  ( B  i^i  A )  C_  B
31, 2eqsstr3i 3381 1  |-  ( A  i^i  B )  C_  B
Colors of variables: wff set class
Syntax hints:    i^i cin 3321    C_ wss 3322
This theorem is referenced by:  difin0  3703  ordin  4614  onfr  4623  ordelinel  4683  relin2  4996  relres  5177  ssrnres  5312  cnvcnv  5326  fnresin2  5563  fresaunres2  5618  ssimaex  5791  exfo  5890  ffvresb  5903  ofrfval  6316  ofval  6317  ofrval  6318  offres  6322  off  6323  ofres  6324  ofco  6327  fnwelem  6464  fnse  6466  tpostpos  6502  smores3  6618  erinxp  6981  pmresg  7044  nnfi  7302  ixpfi2  7408  f1opwfi  7413  dffi2  7431  elfiun  7438  marypha1lem  7441  ordtypelem3  7492  ordtypelem6  7495  ordtypelem7  7496  hartogslem1  7514  unxpwdom  7560  epfrs  7670  tcmin  7683  bnd2  7822  tskwe  7842  r0weon  7899  infxpenlem  7900  fodomfi2  7946  infpwfien  7948  cdainf  8077  ackbij1lem6  8110  ackbij1lem9  8113  ackbij1lem10  8114  ackbij1lem11  8115  ackbij1lem15  8119  ackbij1lem16  8120  ackbij1lem18  8122  ackbij1b  8124  sdom2en01  8187  fin23lem26  8210  fin23lem13  8217  isfin1-3  8271  fin56  8278  fin1a2lem9  8293  ttukeylem6  8399  brdom3  8411  brdom5  8412  brdom4  8413  fpwwe2lem8  8517  fpwwe2lem9  8518  fpwwe2lem12  8521  fpwwe2  8523  canthwelem  8530  gruima  8682  ingru  8695  gruina  8698  grur1a  8699  ltrelpi  8771  ltrelnq  8808  nqerf  8812  fzfi  11316  rexanuz  12154  limsupgord  12271  limsupcl  12272  limsupgf  12274  limsupgle  12276  rlimres  12357  lo1res  12358  o1of2  12411  o1rlimmul  12417  ackbijnn  12612  bitsinv1  12959  bitsinvp1  12966  sadcaddlem  12974  sadadd2lem  12976  sadadd3  12978  sadaddlem  12983  sadasslem  12987  sadeq  12989  smuval2  12999  smupval  13005  smueqlem  13007  prmrec  13295  isstruct2  13483  structcnvcnv  13485  ressbasss  13526  ressress  13531  restsspw  13664  pwsle  13719  submre  13835  isacs2  13883  isacs1i  13887  sscres  14028  rescabs  14038  resscat  14054  funcres2c  14103  coffth  14138  rescfth  14139  ressffth  14140  catccatid  14262  catcisolem  14266  catciso  14267  catcoppccl  14268  catcfuccl  14269  catcxpccl  14309  yoniso  14387  isdrs2  14401  isacs3lem  14597  acsinfd  14611  acsdomd  14612  psssdm2  14652  tsrss  14660  sylow2a  15258  lsmmod  15312  frgpnabllem2  15490  subrgpropd  15907  lssacs  16048  sralmod  16263  asplss  16393  ressmplbas  16524  subrgmpl  16528  opsrtoslem2  16550  mplind  16567  ressply1bas  16628  zlpirlem2  16774  zlpirlem3  16775  basdif0  17023  eltg4i  17030  ntrss2  17126  ntrin  17130  isopn3  17135  mreclatdemo  17165  neiptoptop  17200  restbas  17227  resttopon  17230  restuni2  17236  restcld  17241  restfpw  17248  neitr  17249  ordtrest  17271  subbascn  17323  cnrest2r  17356  cnpresti  17357  cnprest  17358  lmss  17367  cnrmi  17429  restcnrm  17431  resthauslem  17432  fincmp  17461  imacmp  17465  fiuncmp  17472  cmpfi  17476  cnconn  17490  iuncon  17496  clscon  17498  concompclo  17503  1stcrest  17521  subislly  17549  islly2  17552  cldllycmp  17563  hauspwdom  17569  kgeni  17574  llycmpkgen2  17587  1stckgenlem  17590  ptbasfi  17618  txcls  17641  ptclsg  17652  txcnp  17657  ptcnplem  17658  txtube  17677  txcmplem1  17678  txcmplem2  17679  txkgen  17689  xkopt  17692  xkococnlem  17696  txcon  17726  basqtop  17748  tgqtop  17749  kqdisj  17769  kqnrmlem1  17780  kqnrmlem2  17781  nrmhmph  17831  infil  17900  fbasrn  17921  trfg  17928  uzrest  17934  isufil2  17945  fmfnfmlem4  17994  hauspwpwf1  18024  txflf  18043  alexsubALTlem3  18085  alexsubALTlem4  18086  ptcmplem2  18089  tmdgsum2  18131  tsmsres  18178  tsmsxplem1  18187  ustexsym  18250  ustund  18256  trust  18264  utoptop  18269  restutop  18272  blres  18466  met2ndci  18557  metrest  18559  restmetu  18622  tgioo  18832  zdis  18852  reconnlem2  18863  reconn  18864  cnheibor  18985  lebnum  18994  nmoleub2lem3  19128  nmoleub3  19132  cphsqrcl  19152  tchcph  19199  cfilresi  19253  cfilres  19254  caussi  19255  causs  19256  minveclem4b  19337  minveclem4  19338  ovolfcl  19368  ovolfioo  19369  ovolficc  19370  ovolficcss  19371  ovolfsval  19372  ovolfsf  19373  ovollb  19380  ovoliunlem1  19403  ovolicc2lem1  19418  ovolicc2lem2  19419  ovolicc2lem3  19420  ovolicc2lem4  19421  ovolicc2lem5  19422  ovolicc2  19423  nulmbl  19435  voliunlem1  19449  ioombl1lem4  19460  ovolfs2  19468  uniiccdif  19475  uniioovol  19476  uniiccvol  19477  uniioombllem2a  19479  uniioombllem2  19480  uniioombllem3a  19481  uniioombllem3  19482  uniioombllem4  19483  uniioombllem5  19484  uniioombllem6  19485  uniioombl  19486  dyadmbllem  19496  dyadmbl  19497  opnmbllem  19498  volcn  19503  volivth  19504  vitalilem2  19506  vitalilem4  19508  mbfadd  19556  mbfsub  19557  i1fima  19573  i1fima2  19574  i1fd  19576  i1fadd  19590  i1fmul  19591  itg1addlem2  19592  itg1addlem4  19594  itg1addlem5  19595  i1fres  19600  mbfmul  19621  itg2cnlem2  19657  bddmulibl  19733  ellimc2  19769  ellimc3  19771  limcflf  19773  limcresi  19777  limciun  19786  dvreslem  19801  dvres2lem  19802  dvres3a  19806  cpnres  19828  dvaddbr  19829  dvmulbr  19830  dvmptres3  19847  lhop1lem  19902  pf1rcl  19974  ig1peu  20099  taylfvallem1  20278  tayl0  20283  rlimcnp2  20810  xrlimcnp  20812  ppisval  20891  chtf  20896  efchtcl  20899  chtge0  20900  ppinprm  20940  chtprm  20941  chtnprm  20942  chtwordi  20944  chtdif  20946  efchtdvds  20947  chtlepsi  20995  chtleppi  20999  pclogsum  21004  chpval2  21007  chpchtsum  21008  chpub  21009  2sqlem8  21161  2sqlem9  21162  chebbnd1lem1  21168  chtppilimlem1  21172  rplogsumlem2  21184  rpvmasumlem  21186  rplogsum  21226  dirith2  21227  issubgo  21896  opidon  21915  chdmm1i  22984  chm0i  22997  ledii  23043  lejdii  23045  pjoml2i  23092  pjoml4i  23094  cmcmlem  23098  cmbr4i  23108  osumcori  23150  pjssmii  23188  mayete3i  23235  mayete3iOLD  23236  riesz4  23572  riesz1  23573  cnlnadjeu  23586  nmopadjlei  23596  pjclem1  23703  pjci  23708  mdbr3  23805  mdbr4  23806  dmdbr2  23811  dmdbr5  23816  ssmd2  23820  mdslj1i  23827  mdslj2i  23828  mdsl1i  23829  mdsl2bi  23831  mdslmd1lem1  23833  mdslmd1lem2  23834  mdslmd2i  23838  csmdsymi  23842  cvexchlem  23876  atomli  23890  atcvat4i  23905  disjxpin  24033  imadifxp  24043  suppss2f  24054  off2  24059  partfun  24092  resspos  24192  resstos  24193  subofld  24250  pnfneige0  24341  lmxrge0  24342  qqhnm  24379  qqhcn  24380  rrhre  24392  indf1ofs  24428  gsumesum  24456  esumlub  24457  esumcst  24460  esumpcvgval  24473  hasheuni  24480  esumcvg  24481  sigainb  24524  measunl  24575  sibfof  24659  probdif  24683  probmeasb  24693  cndprob01  24698  conpcon  24927  iccllyscon  24942  cvmsss2  24966  cvmcov2  24967  cvmopnlem  24970  cvmliftmolem2  24974  cvmlift2lem12  25006  nepss  25180  dedekindle  25193  elrn3  25391  dfon2lem4  25418  wfrlem4  25546  frrlem4  25590  heicant  26253  opnmbllem0  26254  mblfinlem4  26258  mbfposadd  26266  trer  26333  neiin  26349  neibastop1  26402  neibastop2lem  26403  topmeet  26407  filnetlem3  26423  heibor1lem  26532  heiborlem1  26534  heiborlem3  26536  heiborlem10  26543  elrfi  26762  elrfirn  26763  fnwe2lem2  27140  aomclem2  27144  lsmfgcl  27163  lmhmfgima  27173  lmhmfgsplit  27175  lmhmlnmsplit  27176  uvcff  27231  hbt  27325  mvdco  27379  acsfn1p  27498  onfrALTlem3  28704  onfrALTlem2  28706  onfrALTlem3VD  29073  onfrALTlem2VD  29075  iunconlem2  29121  bnj1293  29262  lshpinN  29861  lcvexchlem1  29906  lcvexchlem5  29910  pmod1i  30719  pmodN  30721  osumcllem7N  30833  pexmidlem4N  30844  dochdmj1  32262  dochexmidlem4  32335  lcfrlem25  32439  mapd1o  32520  mapdin  32534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator