Theorem supex 9476

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459   Or wor 5560  supcsup 9452

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-pr 5402  ax-un 7729

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 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rmo 3359  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-po 5561  df-so 5562  df-sup 9454

This theorem is referenced by:  limsupgval  15492  limsupgre  15497  gcdval  16515  pczpre  16867  prmreclem1  16936  prdsdsfn  17479  prdsdsval  17492  xrge0tsms2  24775  mbfsup  25617  mbfinf  25618  itg2val  25681  itg2monolem1  25703  itg2mono  25706  mdegval  26020  mdegxrf  26025  plyeq0lem  26167  dgrval  26185  nmooval  30744  nmopval  31837  nmfnval  31857  lmdvg  33984  esumval  34077  erdszelem3  35215  erdszelem6  35218  supcnvlimsup  45769  limsuplt2  45782  liminfval  45788  limsupge  45790  liminflelimsuplem  45804  fourierdlem79  46214  sge0val  46395  sge0tsms  46409  smflimsuplem1  46849  smflimsuplem2  46850  smflimsuplem4  46852  fsupdm2  46872