Theorem supex 9057

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

Syntax hints:   ∈ wcel 2112  Vcvv 3398   Or wor 5452  supcsup 9034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ral 3056  df-rex 3057  df-rmo 3059  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-po 5453  df-so 5454  df-sup 9036

This theorem is referenced by:  limsupgval  15002  limsupgre  15007  gcdval  16018  pczpre  16363  prmreclem1  16432  prdsdsfn  16924  prdsdsval  16937  xrge0tsms2  23686  mbfsup  24515  mbfinf  24516  itg2val  24580  itg2monolem1  24602  itg2mono  24605  mdegval  24915  mdegxrf  24920  plyeq0lem  25058  dgrval  25076  nmooval  28798  nmopval  29891  nmfnval  29911  lmdvg  31571  esumval  31680  erdszelem3  32822  erdszelem6  32825  supcnvlimsup  42899  limsuplt2  42912  liminfval  42918  limsupge  42920  liminflelimsuplem  42934  fourierdlem79  43344  sge0val  43522  sge0tsms  43536  smflimsuplem1  43968  smflimsuplem2  43969  smflimsuplem4  43971