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

Theorem sseqin2 3401
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 3386 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  dfss4  3416  resabs1  5000  rescnvcnv  5151  fiint  7149  infxpenlem  7657  ackbij1lem2  7863  nn0supp  10033  uzin  10276  iooval2  10705  fzval2  10801  fz1isolem  11415  dfphi2  12858  ressbas  13214  ressress  13221  sylow3lem2  14955  gsumxp  15243  pgpfac1lem5  15330  cmpsub  17143  fbasrn  17595  cmmbl  18908  voliunlem3  18925  0plef  19043  0pledm  19044  itg1ge0  19057  mbfi1fseqlem5  19090  itg2addlem  19129  dvcmulf  19310  efopn  20021  cmcmlem  22186  pjvec  22291  pjocvec  22292  ssmd2  22908  mdslmd4i  22929  chirredlem2  22987  chirredlem3  22988  dmdbr7ati  23020  lmxrge0  23390  orvcelval  23684  dfon2lem4  24213  sspred  24245  predon  24264  wfrlem4  24330  frrlem4  24355  blssp  26573  fsuppeq  27362  lcvexchlem1  29846  glbconN  30188  pmapglb2N  30582  pmapglb2xN  30583  2polssN  30726  polatN  30742  osumcllem1N  30767  osumcllem9N  30775  pexmidlem6N  30786  diarnN  31941  dihmeetlem11N  32129  dochexmidlem6  32277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator