Theorem supex 9422

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   Or wor 5548  supcsup 9398

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-pr 5390  ax-un 7714

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 2066  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rmo 3356  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-po 5549  df-so 5550  df-sup 9400

This theorem is referenced by:  limsupgval  15449  limsupgre  15454  gcdval  16473  pczpre  16825  prmreclem1  16894  prdsdsfn  17435  prdsdsval  17448  xrge0tsms2  24731  mbfsup  25572  mbfinf  25573  itg2val  25636  itg2monolem1  25658  itg2mono  25661  mdegval  25975  mdegxrf  25980  plyeq0lem  26122  dgrval  26140  nmooval  30699  nmopval  31792  nmfnval  31812  lmdvg  33950  esumval  34043  erdszelem3  35187  erdszelem6  35190  supcnvlimsup  45745  limsuplt2  45758  liminfval  45764  limsupge  45766  liminflelimsuplem  45780  fourierdlem79  46190  sge0val  46371  sge0tsms  46385  smflimsuplem1  46825  smflimsuplem2  46826  smflimsuplem4  46828  fsupdm2  46848