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

Theorem sseqin2 3388
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 3373 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  dfss4  3403  resabs1  4984  rescnvcnv  5135  fiint  7133  infxpenlem  7641  ackbij1lem2  7847  nn0supp  10017  uzin  10260  iooval2  10689  fzval2  10785  fz1isolem  11399  dfphi2  12842  ressbas  13198  ressress  13205  sylow3lem2  14939  gsumxp  15227  pgpfac1lem5  15314  cmpsub  17127  fbasrn  17579  cmmbl  18892  voliunlem3  18909  0plef  19027  0pledm  19028  itg1ge0  19041  mbfi1fseqlem5  19074  itg2addlem  19113  dvcmulf  19294  efopn  20005  cmcmlem  22170  pjvec  22275  pjocvec  22276  ssmd2  22892  mdslmd4i  22913  chirredlem2  22971  chirredlem3  22972  dmdbr7ati  23004  lmxrge0  23375  orvcelval  23669  dfon2lem4  24142  sspred  24174  predon  24193  wfrlem4  24259  frrlem4  24284  blssp  26470  fsuppeq  27259  lcvexchlem1  29224  glbconN  29566  pmapglb2N  29960  pmapglb2xN  29961  2polssN  30104  polatN  30120  osumcllem1N  30145  osumcllem9N  30153  pexmidlem6N  30164  diarnN  31319  dihmeetlem11N  31507  dochexmidlem6  31655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator