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

Theorem ssintub 4493
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 4491 . 2 (𝐴 {𝑥𝐵𝐴𝑥} ↔ ∀𝑦 ∈ {𝑥𝐵𝐴𝑥}𝐴𝑦)
2 sseq2 3625 . . . 4 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
32elrab 3361 . . 3 (𝑦 ∈ {𝑥𝐵𝐴𝑥} ↔ (𝑦𝐵𝐴𝑦))
43simprbi 480 . 2 (𝑦 ∈ {𝑥𝐵𝐴𝑥} → 𝐴𝑦)
51, 4mprgbir 2926 1 𝐴 {𝑥𝐵𝐴𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  {crab 2915  wss 3572   cint 4473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rab 2920  df-v 3200  df-in 3579  df-ss 3586  df-int 4474
This theorem is referenced by:  intmin  4495  wuncid  9562  mrcssid  16271  lspssid  18979  lbsextlem3  19154  aspssid  19327  sscls  20854  filufint  21718  spanss2  28188  shsval2i  28230  ococin  28251  chsupsn  28256  sssigagen  30193  dynkin  30215  igenss  33841  pclssidN  35007  dochocss  36481  rgspnssid  37566
  Copyright terms: Public domain W3C validator