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

Theorem sseqin2 3624
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 3610 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437    i^i cin 3378    C_ wss 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386  df-ss 3393
This theorem is referenced by:  dfss4  3650  resabs1  5095  rescnvcnv  5260  sspred  5350  predon  6576  frnsuppeq  6881  wfrlem4  6994  fiint  7801  infxpenlem  8396  ackbij1lem2  8602  uzin  11142  iooval2  11620  fzval2  11738  fz1isolem  12572  dfphi2  14665  ressbas  15122  ressress  15130  sylow3lem2  17223  gsumxp  17551  pgpfac1lem5  17655  cmpsub  20357  fbasrn  20841  cmmbl  22430  voliunlem3  22447  0plef  22572  0pledm  22573  itg1ge0  22586  mbfi1fseqlem5  22619  itg2addlem  22658  dvcmulf  22841  efopn  23545  cmcmlem  27186  pjvec  27291  pjocvec  27292  ssmd2  27907  mdslmd4i  27928  chirredlem2  27986  chirredlem3  27987  dmdbr7ati  28019  lmxrge0  28710  orvcelval  29253  dfon2lem4  30383  frrlem4  30468  mblfinlem3  31886  blssp  31992  lcvexchlem1  32512  glbconN  32854  pmapglb2N  33248  pmapglb2xN  33249  2polssN  33392  polatN  33408  osumcllem1N  33433  osumcllem9N  33441  pexmidlem6N  33452  dihmeetlem11N  34797  dochexmidlem6  34945
  Copyright terms: Public domain W3C validator