Theorem supex 9425

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   Or wor 5570  supcsup 9401

This theorem was proved from 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 5258  ax-pr 5406  ax-un 7734

This theorem 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 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-po 5571  df-so 5572  df-sup 9403

This theorem is referenced by:  limsupgval  15529  limsupgre  15534  gcdval  16555  pczpre  16908  prmreclem1  16977  prdsdsfn  17519  prdsdsval  17532  xrge0tsms2  24974  mbfsup  25804  mbfinf  25805  itg2val  25868  itg2monolem1  25890  itg2mono  25893  mdegval  26201  mdegxrf  26206  plyeq0lem  26348  dgrval  26366  nmooval  31096  nmopval  32189  nmfnval  32209  lmdvg  34324  esumval  34417  erdszelem3  35666  erdszelem6  35669  supcnvlimsup  46437  limsuplt2  46450  liminfval  46456  limsupge  46458  liminflelimsuplem  46472  fourierdlem79  46882  sge0val  47063  sge0tsms  47077  smflimsuplem1  47517  smflimsuplem2  47518  smflimsuplem4  47520  fsupdm2  47540