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

Theorem ssintub 4304
Description: Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
Assertion
Ref Expression
ssintub
Distinct variable groups:   ,   ,

Proof of Theorem ssintub
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssint 4302 . 2
2 sseq2 3525 . . . 4
32elrab 3257 . . 3
43simprbi 464 . 2
51, 4mprgbir 2821 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  {crab 2811  C_wss 3475  |^|cint 4286
This theorem is referenced by:  intmin  4306  wuncid  9142  mrcssid  15014  lspssid  17631  lbsextlem3  17806  aspssid  17982  sscls  19557  filufint  20421  spanss2  26263  shsval2i  26305  ococin  26326  chsupsn  26331  sssigagen  28145  igenss  30459  rgspnssid  31119  pclssidN  35619  dochocss  37093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rab 2816  df-v 3111  df-in 3482  df-ss 3489  df-int 4287
  Copyright terms: Public domain W3C validator