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

Theorem sseqin2 3678
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 3664 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1370    i^i cin 3436    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3444  df-ss 3451
This theorem is referenced by:  dfss4  3693  resabs1  5248  rescnvcnv  5410  frnsuppeq  6813  fiint  7700  infxpenlem  8292  ackbij1lem2  8502  nn0suppOLD  10746  uzin  11005  iooval2  11445  fzval2  11558  fz1isolem  12333  dfphi2  13968  ressbas  14348  ressress  14355  sylow3lem2  16249  gsumxp  16591  gsumxpOLD  16593  pgpfac1lem5  16703  cmpsub  19136  fbasrn  19590  cmmbl  21150  voliunlem3  21167  0plef  21284  0pledm  21285  itg1ge0  21298  mbfi1fseqlem5  21331  itg2addlem  21370  dvcmulf  21553  efopn  22237  cmcmlem  25147  pjvec  25252  pjocvec  25253  ssmd2  25869  mdslmd4i  25890  chirredlem2  25948  chirredlem3  25949  dmdbr7ati  25981  lmxrge0  26528  orvcelval  26996  dfon2lem4  27744  sspred  27778  predon  27799  wfrlem4  27872  frrlem4  27916  mblfinlem3  28579  blssp  28801  fsuppeq  29599  lcvexchlem1  33018  glbconN  33360  pmapglb2N  33754  pmapglb2xN  33755  2polssN  33898  polatN  33914  osumcllem1N  33939  osumcllem9N  33947  pexmidlem6N  33958  dihmeetlem11N  35301  dochexmidlem6  35449
  Copyright terms: Public domain W3C validator