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

Theorem sseqin2 3564
Description: A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
Assertion
Ref Expression
sseqin2  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )

Proof of Theorem sseqin2
StepHypRef Expression
1 dfss1 3550 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369    i^i cin 3322    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337
This theorem is referenced by:  dfss4  3579  resabs1  5134  rescnvcnv  5296  frnsuppeq  6697  fiint  7580  infxpenlem  8172  ackbij1lem2  8382  nn0suppOLD  10626  uzin  10885  iooval2  11325  fzval2  11432  fz1isolem  12206  dfphi2  13841  ressbas  14220  ressress  14227  sylow3lem2  16118  gsumxp  16456  gsumxpOLD  16458  pgpfac1lem5  16568  cmpsub  18978  fbasrn  19432  cmmbl  20991  voliunlem3  21008  0plef  21125  0pledm  21126  itg1ge0  21139  mbfi1fseqlem5  21172  itg2addlem  21211  dvcmulf  21394  efopn  22078  cmcmlem  24945  pjvec  25050  pjocvec  25051  ssmd2  25667  mdslmd4i  25688  chirredlem2  25746  chirredlem3  25747  dmdbr7ati  25779  lmxrge0  26334  orvcelval  26803  dfon2lem4  27550  sspred  27584  predon  27605  wfrlem4  27678  frrlem4  27722  mblfinlem3  28383  blssp  28605  fsuppeq  29403  lcvexchlem1  32519  glbconN  32861  pmapglb2N  33255  pmapglb2xN  33256  2polssN  33399  polatN  33415  osumcllem1N  33440  osumcllem9N  33448  pexmidlem6N  33459  dihmeetlem11N  34802  dochexmidlem6  34950
  Copyright terms: Public domain W3C validator