Theorem supex 9420

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

This proof depends on syntax axioms:   ∈ wcel 2143  Vcvv 3455   Or wor 5568  supcsup 9396

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rmo 3369  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-po 5569  df-so 5570  df-sup 9398

This theorem is used by:  limsupgval  15532  limsupgre  15537  gcdval  16558  pczpre  16911  prmreclem1  16980  prdsdsfn  17522  prdsdsval  17535  xrge0tsms2  25002  mbfsup  25832  mbfinf  25833  itg2val  25896  itg2monolem1  25918  itg2mono  25921  mdegval  26229  mdegxrf  26234  plyeq0lem  26376  dgrval  26394  nmooval  31124  nmopval  32217  nmfnval  32237  lmdvg  34352  esumval  34445  erdszelem3  35693  erdszelem6  35696  supcnvlimsup  46482  limsuplt2  46495  liminfval  46501  limsupge  46503  liminflelimsuplem  46517  fourierdlem79  46927  sge0val  47108  sge0tsms  47122  smflimsuplem1  47562  smflimsuplem2  47563  smflimsuplem4  47565  fsupdm2  47585