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

Theorem ssintub 4963
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 4961 . 2 (𝐴 {𝑥𝐵𝐴𝑥} ↔ ∀𝑦 ∈ {𝑥𝐵𝐴𝑥}𝐴𝑦)
2 sseq2 4003 . . . 4 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
32elrab 3678 . . 3 (𝑦 ∈ {𝑥𝐵𝐴𝑥} ↔ (𝑦𝐵𝐴𝑦))
43simprbi 496 . 2 (𝑦 ∈ {𝑥𝐵𝐴𝑥} → 𝐴𝑦)
51, 4mprgbir 3062 1 𝐴 {𝑥𝐵𝐴𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2098  {crab 3426  wss 3943   cint 4943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-11 2146  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ral 3056  df-rab 3427  df-v 3470  df-in 3950  df-ss 3960  df-int 4944
This theorem is referenced by:  intmin  4965  cofon2  8674  naddunif  8694  wuncid  10740  mrcssid  17570  lspssid  20832  lbsextlem3  21011  aspssid  21772  sscls  22915  filufint  23779  spanss2  31107  shsval2i  31149  ococin  31170  chsupsn  31175  fldgenssid  32906  sssigagen  33673  dynkin  33695  igenss  37443  pclssidN  39279  dochocss  40750  rgspnssid  42487  intubeu  47880
  Copyright terms: Public domain W3C validator