Theorem supex 9493

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   Or wor 5565  supcsup 9469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rmo 3369  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-po 5566  df-so 5567  df-sup 9471

This theorem is used by:  limsupgval  15687  limsupgre  15692  gcdval  16710  pczpre  17069  prmreclem1  17138  prdsdsfn  17686  prdsdsval  17699  xrge0tsms2  25210  mbfsup  26040  mbfinf  26041  itg2val  26104  itg2monolem1  26126  itg2mono  26129  mdegval  26436  mdegxrf  26441  plyeq0lem  26584  dgrval  26602  nmooval  31422  nmopval  32515  nmfnval  32535  lmdvg  34696  esumval  34789  erdszelem3  36166  erdszelem6  36169  supcnvlimsup  47023  limsuplt2  47036  liminfval  47042  limsupge  47044  liminflelimsuplem  47058  fourierdlem79  47468  sge0val  47649  sge0tsms  47663  smflimsuplem1  48103  smflimsuplem2  48104  smflimsuplem4  48106  fsupdm2  48126