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

Theorem ssintub 4289
Description: Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
Assertion
Ref Expression
ssintub  |-  A  C_  |^|
{ x  e.  B  |  A  C_  x }
Distinct variable groups:    x, A    x, B

Proof of Theorem ssintub
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ssint 4287 . 2  |-  ( A 
C_  |^| { x  e.  B  |  A  C_  x }  <->  A. y  e.  {
x  e.  B  |  A  C_  x } A  C_  y )
2 sseq2 3511 . . . 4  |-  ( x  =  y  ->  ( A  C_  x  <->  A  C_  y
) )
32elrab 3243 . . 3  |-  ( y  e.  { x  e.  B  |  A  C_  x }  <->  ( y  e.  B  /\  A  C_  y ) )
43simprbi 464 . 2  |-  ( y  e.  { x  e.  B  |  A  C_  x }  ->  A  C_  y )
51, 4mprgbir 2807 1  |-  A  C_  |^|
{ x  e.  B  |  A  C_  x }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   {crab 2797    C_ wss 3461   |^|cint 4271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rab 2802  df-v 3097  df-in 3468  df-ss 3475  df-int 4272
This theorem is referenced by:  intmin  4291  wuncid  9124  mrcssid  14891  lspssid  17505  lbsextlem3  17680  aspssid  17856  sscls  19430  filufint  20294  spanss2  26135  shsval2i  26177  ococin  26198  chsupsn  26203  sssigagen  28018  igenss  30434  rgspnssid  31095  pclssidN  35353  dochocss  36827
  Copyright terms: Public domain W3C validator