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

Theorem sseqin2 3524
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 3509 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    i^i cin 3283    C_ wss 3284
This theorem is referenced by:  dfss4  3539  resabs1  5138  rescnvcnv  5295  fiint  7346  infxpenlem  7855  ackbij1lem2  8061  nn0supp  10233  uzin  10478  iooval2  10909  fzval2  11006  fz1isolem  11669  dfphi2  13122  ressbas  13478  ressress  13485  sylow3lem2  15221  gsumxp  15509  pgpfac1lem5  15596  cmpsub  17421  fbasrn  17873  cmmbl  19386  voliunlem3  19403  0plef  19521  0pledm  19522  itg1ge0  19535  mbfi1fseqlem5  19568  itg2addlem  19607  dvcmulf  19788  efopn  20506  cmcmlem  23050  pjvec  23155  pjocvec  23156  ssmd2  23772  mdslmd4i  23793  chirredlem2  23851  chirredlem3  23852  dmdbr7ati  23884  lmxrge0  24294  orvcelval  24683  dfon2lem4  25360  sspred  25392  predon  25411  wfrlem4  25477  frrlem4  25502  mblfinlem2  26148  blssp  26356  fsuppeq  27131  lcvexchlem1  29521  glbconN  29863  pmapglb2N  30257  pmapglb2xN  30258  2polssN  30401  polatN  30417  osumcllem1N  30442  osumcllem9N  30450  pexmidlem6N  30461  dihmeetlem11N  31804  dochexmidlem6  31952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-in 3291  df-ss 3298
  Copyright terms: Public domain W3C validator