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

Theorem sseqin2 3363
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 3348 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    i^i cin 3126    C_ wss 3127
This theorem is referenced by:  dfss4  3378  resabs1  4972  rescnvcnv  5122  fiint  7101  infxpenlem  7609  ackbij1lem2  7815  nn0supp  9985  uzin  10228  iooval2  10656  fzval2  10752  fz1isolem  11365  dfphi2  12805  ressbas  13161  ressress  13168  sylow3lem2  14902  gsumxp  15190  pgpfac1lem5  15277  cmpsub  17090  fbasrn  17542  cmmbl  18855  voliunlem3  18872  0plef  18990  0pledm  18991  itg1ge0  19004  mbfi1fseqlem5  19037  itg2addlem  19076  dvcmulf  19257  efopn  19968  cmcmlem  22131  pjvec  22236  pjocvec  22237  ssmd2  22853  mdslmd4i  22874  chirredlem2  22932  chirredlem3  22933  dmdbr7ati  22965  dfon2lem4  23512  sspred  23544  predon  23563  wfrlem4  23629  frrlem4  23654  axfelem20  23735  blssp  25838  fsuppeq  26627  lcvexchlem1  28474  glbconN  28816  pmapglb2N  29210  pmapglb2xN  29211  2polssN  29354  polatN  29370  osumcllem1N  29395  osumcllem9N  29403  pexmidlem6N  29414  diarnN  30569  dihmeetlem11N  30757  dochexmidlem6  30905
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator