Theorem supex 9379

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442   Or wor 5539  supcsup 9355

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rmo 3352  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-po 5540  df-so 5541  df-sup 9357

This theorem is referenced by:  limsupgval  15411  limsupgre  15416  gcdval  16435  pczpre  16787  prmreclem1  16856  prdsdsfn  17397  prdsdsval  17410  xrge0tsms2  24792  mbfsup  25633  mbfinf  25634  itg2val  25697  itg2monolem1  25719  itg2mono  25722  mdegval  26036  mdegxrf  26041  plyeq0lem  26183  dgrval  26201  nmooval  30850  nmopval  31943  nmfnval  31963  lmdvg  34130  esumval  34223  erdszelem3  35406  erdszelem6  35409  supcnvlimsup  46092  limsuplt2  46105  liminfval  46111  limsupge  46113  liminflelimsuplem  46127  fourierdlem79  46537  sge0val  46718  sge0tsms  46732  smflimsuplem1  47172  smflimsuplem2  47173  smflimsuplem4  47175  fsupdm2  47195