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

Theorem sseqin2 3703
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 3689 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1398    i^i cin 3460    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475
This theorem is referenced by:  dfss4  3729  resabs1  5290  rescnvcnv  5453  frnsuppeq  6903  fiint  7789  infxpenlem  8382  ackbij1lem2  8592  nn0suppOLD  10846  uzin  11114  iooval2  11565  fzval2  11678  fz1isolem  12494  dfphi2  14388  ressbas  14773  ressress  14781  sylow3lem2  16847  gsumxp  17200  pgpfac1lem5  17325  cmpsub  20067  fbasrn  20551  cmmbl  22111  voliunlem3  22128  0plef  22245  0pledm  22246  itg1ge0  22259  mbfi1fseqlem5  22292  itg2addlem  22331  dvcmulf  22514  efopn  23207  cmcmlem  26707  pjvec  26812  pjocvec  26813  ssmd2  27429  mdslmd4i  27450  chirredlem2  27508  chirredlem3  27509  dmdbr7ati  27541  lmxrge0  28169  orvcelval  28671  dfon2lem4  29458  sspred  29492  predon  29513  wfrlem4  29586  frrlem4  29630  mblfinlem3  30293  blssp  30489  fsuppeq  31282  lcvexchlem1  35156  glbconN  35498  pmapglb2N  35892  pmapglb2xN  35893  2polssN  36036  polatN  36052  osumcllem1N  36077  osumcllem9N  36085  pexmidlem6N  36096  dihmeetlem11N  37441  dochexmidlem6  37589
  Copyright terms: Public domain W3C validator