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

Theorem sseqin2 3330
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 3315 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    i^i cin 3093    C_ wss 3094
This theorem is referenced by:  dfss4  3345  resabs1  4937  rescnvcnv  5087  fiint  7066  infxpenlem  7574  ackbij1lem2  7780  nn0supp  9949  uzin  10192  iooval2  10620  fzval2  10716  fz1isolem  11329  dfphi2  12769  ressbas  13125  ressress  13132  sylow3lem2  14866  gsumxp  15154  pgpfac1lem5  15241  cmpsub  17054  fbasrn  17506  cmmbl  18819  voliunlem3  18836  0plef  18954  0pledm  18955  itg1ge0  18968  mbfi1fseqlem5  19001  itg2addlem  19040  dvcmulf  19221  efopn  19932  cmcmlem  22113  pjvec  22218  pjocvec  22219  ssmd2  22817  mdslmd4i  22838  chirredlem2  22896  chirredlem3  22897  dmdbr7ati  22929  dfon2lem4  23476  sspred  23508  predon  23527  wfrlem4  23593  frrlem4  23618  axfelem20  23699  blssp  25802  fsuppeq  26591  lcvexchlem1  28354  glbconN  28696  pmapglb2N  29090  pmapglb2xN  29091  2polssN  29234  polatN  29250  osumcllem1N  29275  osumcllem9N  29283  pexmidlem6N  29294  diarnN  30449  dihmeetlem11N  30637  dochexmidlem6  30785
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator