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

Theorem sseqin2 3389
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 3374 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    i^i cin 3152    C_ wss 3153
This theorem is referenced by:  dfss4  3404  resabs1  4983  rescnvcnv  5133  fiint  7129  infxpenlem  7637  ackbij1lem2  7843  nn0supp  10013  uzin  10256  iooval2  10685  fzval2  10781  fz1isolem  11395  dfphi2  12838  ressbas  13194  ressress  13201  sylow3lem2  14935  gsumxp  15223  pgpfac1lem5  15310  cmpsub  17123  fbasrn  17575  cmmbl  18888  voliunlem3  18905  0plef  19023  0pledm  19024  itg1ge0  19037  mbfi1fseqlem5  19070  itg2addlem  19109  dvcmulf  19290  efopn  20001  cmcmlem  22166  pjvec  22271  pjocvec  22272  ssmd2  22888  mdslmd4i  22909  chirredlem2  22967  chirredlem3  22968  dmdbr7ati  23000  dfon2lem4  23546  sspred  23578  predon  23597  wfrlem4  23663  frrlem4  23688  axfelem20  23769  blssp  25881  fsuppeq  26670  lcvexchlem1  28503  glbconN  28845  pmapglb2N  29239  pmapglb2xN  29240  2polssN  29383  polatN  29399  osumcllem1N  29424  osumcllem9N  29432  pexmidlem6N  29443  diarnN  30598  dihmeetlem11N  30786  dochexmidlem6  30934
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator