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

Theorem sseqin2 3390
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 3375 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1625    i^i cin 3153    C_ wss 3154
This theorem is referenced by:  dfss4  3405  resabs1  4986  rescnvcnv  5137  fiint  7135  infxpenlem  7643  ackbij1lem2  7849  nn0supp  10019  uzin  10262  iooval2  10691  fzval2  10787  fz1isolem  11401  dfphi2  12844  ressbas  13200  ressress  13207  sylow3lem2  14941  gsumxp  15229  pgpfac1lem5  15316  cmpsub  17129  fbasrn  17581  cmmbl  18894  voliunlem3  18911  0plef  19029  0pledm  19030  itg1ge0  19043  mbfi1fseqlem5  19076  itg2addlem  19115  dvcmulf  19296  efopn  20007  cmcmlem  22172  pjvec  22277  pjocvec  22278  ssmd2  22894  mdslmd4i  22915  chirredlem2  22973  chirredlem3  22974  dmdbr7ati  23006  lmxrge0  23377  orvcelval  23671  dfon2lem4  24144  sspred  24176  predon  24195  wfrlem4  24261  frrlem4  24286  blssp  26481  fsuppeq  27270  lcvexchlem1  29297  glbconN  29639  pmapglb2N  30033  pmapglb2xN  30034  2polssN  30177  polatN  30193  osumcllem1N  30218  osumcllem9N  30226  pexmidlem6N  30237  diarnN  31392  dihmeetlem11N  31580  dochexmidlem6  31728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator