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

Theorem ssintub 4927
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 4925 . 2 (𝐴 {𝑥𝐵𝐴𝑥} ↔ ∀𝑦 ∈ {𝑥𝐵𝐴𝑥}𝐴𝑦)
2 sseq2 3970 . . . 4 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
32elrab 3645 . . 3 (𝑦 ∈ {𝑥𝐵𝐴𝑥} ↔ (𝑦𝐵𝐴𝑦))
43simprbi 497 . 2 (𝑦 ∈ {𝑥𝐵𝐴𝑥} → 𝐴𝑦)
51, 4mprgbir 3071 1 𝐴 {𝑥𝐵𝐴𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  {crab 3407  wss 3910   cint 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rab 3408  df-v 3447  df-in 3917  df-ss 3927  df-int 4908
This theorem is referenced by:  intmin  4929  cofon2  8618  naddunif  8636  wuncid  10678  mrcssid  17496  lspssid  20444  lbsextlem3  20619  aspssid  21279  sscls  22405  filufint  23269  spanss2  30285  shsval2i  30327  ococin  30348  chsupsn  30353  fldgenssid  32077  sssigagen  32735  dynkin  32757  igenss  36512  pclssidN  38349  dochocss  39820  rgspnssid  41475  intubeu  46981
  Copyright terms: Public domain W3C validator