Theorem supex 9427

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457   Or wor 5570  supcsup 9403

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7738

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 2100  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rmo 3371  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-po 5571  df-so 5572  df-sup 9405

This theorem is used by:  limsupgval  15546  limsupgre  15551  gcdval  16571  pczpre  16924  prmreclem1  16993  prdsdsfn  17535  prdsdsval  17548  xrge0tsms2  25022  mbfsup  25852  mbfinf  25853  itg2val  25916  itg2monolem1  25938  itg2mono  25941  mdegval  26249  mdegxrf  26254  plyeq0lem  26396  dgrval  26414  nmooval  31144  nmopval  32237  nmfnval  32257  lmdvg  34366  esumval  34459  erdszelem3  35698  erdszelem6  35701  supcnvlimsup  46487  limsuplt2  46500  liminfval  46506  limsupge  46508  liminflelimsuplem  46522  fourierdlem79  46932  sge0val  47113  sge0tsms  47127  smflimsuplem1  47567  smflimsuplem2  47568  smflimsuplem4  47570  fsupdm2  47590