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

Theorem ssintub 4244
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 4242 . 2  |-  ( A 
C_  |^| { x  e.  B  |  A  C_  x }  <->  A. y  e.  {
x  e.  B  |  A  C_  x } A  C_  y )
2 sseq2 3476 . . . 4  |-  ( x  =  y  ->  ( A  C_  x  <->  A  C_  y
) )
32elrab 3214 . . 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 2894 1  |-  A  C_  |^|
{ x  e.  B  |  A  C_  x }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   {crab 2799    C_ wss 3426   |^|cint 4226
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 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rab 2804  df-v 3070  df-in 3433  df-ss 3440  df-int 4227
This theorem is referenced by:  intmin  4246  wuncid  9011  mrcssid  14657  lspssid  17172  lbsextlem3  17347  aspssid  17510  sscls  18776  filufint  19609  spanss2  24883  shsval2i  24925  ococin  24946  chsupsn  24951  sssigagen  26722  igenss  29000  rgspnssid  29665  pclssidN  33845  dochocss  35317
  Copyright terms: Public domain W3C validator