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

Theorem sseqin2 3295
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 3281 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    i^i cin 3077    C_ wss 3078
This theorem is referenced by:  dfss4  3310  resabs1  4891  rescnvcnv  5041  fiint  7018  infxpenlem  7525  ackbij1lem2  7731  nn0supp  9896  uzin  10139  iooval2  10567  fzval2  10663  fz1isolem  11276  dfphi2  12716  ressbas  13072  ressress  13079  sylow3lem2  14774  gsumxp  15062  pgpfac1lem5  15149  cmpsub  16959  fbasrn  17411  cmmbl  18724  voliunlem3  18741  0plef  18859  0pledm  18860  itg1ge0  18873  mbfi1fseqlem5  18906  itg2addlem  18945  dvcmulf  19126  efopn  19837  cmcmlem  22018  pjvec  22123  pjocvec  22124  ssmd2  22722  mdslmd4i  22743  chirredlem2  22801  chirredlem3  22802  dmdbr7ati  22834  dfon2lem4  23310  sspred  23342  predon  23361  wfrlem4  23427  frrlem4  23452  axfelem20  23533  blssp  25636  fsuppeq  26425  lcvexchlem1  27913  glbconN  28255  pmapglb2N  28649  pmapglb2xN  28650  2polssN  28793  polatN  28809  osumcllem1N  28834  osumcllem9N  28842  pexmidlem6N  28853  diarnN  30008  dihmeetlem11N  30196  dochexmidlem6  30344
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator