Theorem supex 9373

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 22	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Or 𝐴)
3	2	supexd 9362	. 2 ⊢ (𝑅 Or 𝐴 → sup(𝐵, 𝐴, 𝑅) ∈ V)
4	1, 3	ax-mp 5	1 ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3438   Or wor 5530  supcsup 9349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rmo 3345  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-po 5531  df-so 5532  df-sup 9351

This theorem is referenced by:  limsupgval  15401  limsupgre  15406  gcdval  16425  pczpre  16777  prmreclem1  16846  prdsdsfn  17387  prdsdsval  17400  xrge0tsms2  24740  mbfsup  25581  mbfinf  25582  itg2val  25645  itg2monolem1  25667  itg2mono  25670  mdegval  25984  mdegxrf  25989  plyeq0lem  26131  dgrval  26149  nmooval  30725  nmopval  31818  nmfnval  31838  lmdvg  33919  esumval  34012  erdszelem3  35165  erdszelem6  35168  supcnvlimsup  45722  limsuplt2  45735  liminfval  45741  limsupge  45743  liminflelimsuplem  45757  fourierdlem79  46167  sge0val  46348  sge0tsms  46362  smflimsuplem1  46802  smflimsuplem2  46803  smflimsuplem4  46805  fsupdm2  46825