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

Theorem ssintub 4973
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 4971 . 2 (𝐴 {𝑥𝐵𝐴𝑥} ↔ ∀𝑦 ∈ {𝑥𝐵𝐴𝑥}𝐴𝑦)
2 sseq2 4008 . . . 4 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
32elrab 3684 . . 3 (𝑦 ∈ {𝑥𝐵𝐴𝑥} ↔ (𝑦𝐵𝐴𝑦))
43simprbi 495 . 2 (𝑦 ∈ {𝑥𝐵𝐴𝑥} → 𝐴𝑦)
51, 4mprgbir 3065 1 𝐴 {𝑥𝐵𝐴𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2098  {crab 3430  wss 3949   cint 4953
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 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rab 3431  df-v 3475  df-in 3956  df-ss 3966  df-int 4954
This theorem is referenced by:  intmin  4975  cofon2  8700  naddunif  8720  wuncid  10774  mrcssid  17604  lspssid  20876  lbsextlem3  21055  aspssid  21818  sscls  22980  filufint  23844  spanss2  31175  shsval2i  31217  ococin  31238  chsupsn  31243  fldgenssid  33024  sssigagen  33797  dynkin  33819  igenss  37568  pclssidN  39400  dochocss  40871  rgspnssid  42625  intubeu  48073
  Copyright terms: Public domain W3C validator