Theorem supex 9412

Description: A supremum is a set. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
supex.1	⊢ 𝑅 Or 𝐴

Assertion

Ref	Expression
supex	⊢ sup(𝐵, 𝐴, 𝑅) ∈ V

Proof of Theorem supex

Step	Hyp	Ref	Expression
1		supex.1	. 2 ⊢ 𝑅 Or 𝐴
2		id 23	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Or 𝐴)
3	2	supexd 9401	. 2 ⊢ (𝑅 Or 𝐴 → sup(𝐵, 𝐴, 𝑅) ∈ V)
4	1, 3	ax-mp 5	1 ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3457   Or wor 5558  supcsup 9388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rmo 3370  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-po 5559  df-so 5560  df-sup 9390

This theorem is referenced by:  limsupgval  15515  limsupgre  15520  gcdval  16542  pczpre  16895  prmreclem1  16964  prdsdsfn  17506  prdsdsval  17519  xrge0tsms2  24950  mbfsup  25780  mbfinf  25781  itg2val  25844  itg2monolem1  25866  itg2mono  25869  mdegval  26177  mdegxrf  26182  plyeq0lem  26324  dgrval  26342  nmooval  31020  nmopval  32113  nmfnval  32133  lmdvg  34255  esumval  34348  erdszelem3  35551  erdszelem6  35554  supcnvlimsup  46313  limsuplt2  46326  liminfval  46332  limsupge  46334  liminflelimsuplem  46348  fourierdlem79  46758  sge0val  46939  sge0tsms  46953  smflimsuplem1  47393  smflimsuplem2  47394  smflimsuplem4  47396  fsupdm2  47416