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

Theorem sseqin2 3464
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 3449 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1642    i^i cin 3227    C_ wss 3228
This theorem is referenced by:  dfss4  3479  resabs1  5066  rescnvcnv  5217  fiint  7223  infxpenlem  7731  ackbij1lem2  7937  nn0supp  10109  uzin  10352  iooval2  10781  fzval2  10877  fz1isolem  11495  dfphi2  12939  ressbas  13295  ressress  13302  sylow3lem2  15038  gsumxp  15326  pgpfac1lem5  15413  cmpsub  17233  fbasrn  17681  cmmbl  18996  voliunlem3  19013  0plef  19131  0pledm  19132  itg1ge0  19145  mbfi1fseqlem5  19178  itg2addlem  19217  dvcmulf  19398  efopn  20116  cmcmlem  22284  pjvec  22389  pjocvec  22390  ssmd2  23006  mdslmd4i  23027  chirredlem2  23085  chirredlem3  23086  dmdbr7ati  23118  lmxrge0  23493  orvcelval  23975  dfon2lem4  24700  sspred  24732  predon  24751  wfrlem4  24817  frrlem4  24842  blssp  25794  fsuppeq  26582  lcvexchlem1  29293  glbconN  29635  pmapglb2N  30029  pmapglb2xN  30030  2polssN  30173  polatN  30189  osumcllem1N  30214  osumcllem9N  30222  pexmidlem6N  30233  diarnN  31388  dihmeetlem11N  31576  dochexmidlem6  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator