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

Theorem ssintub 4885
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 4883 . 2 (𝐴 {𝑥𝐵𝐴𝑥} ↔ ∀𝑦 ∈ {𝑥𝐵𝐴𝑥}𝐴𝑦)
2 sseq2 3990 . . . 4 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
32elrab 3677 . . 3 (𝑦 ∈ {𝑥𝐵𝐴𝑥} ↔ (𝑦𝐵𝐴𝑦))
43simprbi 497 . 2 (𝑦 ∈ {𝑥𝐵𝐴𝑥} → 𝐴𝑦)
51, 4mprgbir 3150 1 𝐴 {𝑥𝐵𝐴𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  {crab 3139  wss 3933   cint 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rab 3144  df-v 3494  df-in 3940  df-ss 3949  df-int 4868
This theorem is referenced by:  intmin  4887  wuncid  10153  mrcssid  16876  lspssid  19686  lbsextlem3  19861  aspssid  20035  sscls  21592  filufint  22456  spanss2  29049  shsval2i  29091  ococin  29112  chsupsn  29117  sssigagen  31303  dynkin  31325  igenss  35221  pclssidN  36911  dochocss  38382  rgspnssid  39648
  Copyright terms: Public domain W3C validator