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

Theorem sseqin2 3717
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 3703 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379    i^i cin 3475    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  dfss4  3732  resabs1  5300  rescnvcnv  5468  frnsuppeq  6910  fiint  7793  infxpenlem  8387  ackbij1lem2  8597  nn0suppOLD  10846  uzin  11110  iooval2  11558  fzval2  11671  fz1isolem  12472  dfphi2  14159  ressbas  14541  ressress  14548  sylow3lem2  16444  gsumxp  16795  gsumxpOLD  16797  pgpfac1lem5  16920  cmpsub  19666  fbasrn  20120  cmmbl  21680  voliunlem3  21697  0plef  21814  0pledm  21815  itg1ge0  21828  mbfi1fseqlem5  21861  itg2addlem  21900  dvcmulf  22083  efopn  22767  cmcmlem  26185  pjvec  26290  pjocvec  26291  ssmd2  26907  mdslmd4i  26928  chirredlem2  26986  chirredlem3  26987  dmdbr7ati  27019  lmxrge0  27570  orvcelval  28047  dfon2lem4  28795  sspred  28829  predon  28850  wfrlem4  28923  frrlem4  28967  mblfinlem3  29630  blssp  29852  fsuppeq  30647  lcvexchlem1  33831  glbconN  34173  pmapglb2N  34567  pmapglb2xN  34568  2polssN  34711  polatN  34727  osumcllem1N  34752  osumcllem9N  34760  pexmidlem6N  34771  dihmeetlem11N  36114  dochexmidlem6  36262
  Copyright terms: Public domain W3C validator