Theorem supex 9374

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432   Or wor 5532  supcsup 9350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rmo 3345  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-po 5533  df-so 5534  df-sup 9352

This theorem is referenced by:  limsupgval  15436  limsupgre  15441  gcdval  16463  pczpre  16816  prmreclem1  16885  prdsdsfn  17426  prdsdsval  17439  xrge0tsms2  24826  mbfsup  25656  mbfinf  25657  itg2val  25720  itg2monolem1  25742  itg2mono  25745  mdegval  26053  mdegxrf  26058  plyeq0lem  26200  dgrval  26218  nmooval  30859  nmopval  31952  nmfnval  31972  lmdvg  34144  esumval  34237  erdszelem3  35428  erdszelem6  35431  supcnvlimsup  46190  limsuplt2  46203  liminfval  46209  limsupge  46211  liminflelimsuplem  46225  fourierdlem79  46635  sge0val  46816  sge0tsms  46830  smflimsuplem1  47270  smflimsuplem2  47271  smflimsuplem4  47273  fsupdm2  47293