Theorem supex 8927

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494   Or wor 5473  supcsup 8904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rmo 3146  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-po 5474  df-so 5475  df-sup 8906

This theorem is referenced by:  limsupgval  14833  limsupgre  14838  gcdval  15845  pczpre  16184  prmreclem1  16252  prdsdsfn  16738  prdsdsval  16751  xrge0tsms2  23443  mbfsup  24265  mbfinf  24266  itg2val  24329  itg2monolem1  24351  itg2mono  24354  mdegval  24657  mdegxrf  24662  plyeq0lem  24800  dgrval  24818  nmooval  28540  nmopval  29633  nmfnval  29653  lmdvg  31196  esumval  31305  erdszelem3  32440  erdszelem6  32443  supcnvlimsup  42041  limsuplt2  42054  liminfval  42060  limsupge  42062  liminflelimsuplem  42076  fourierdlem79  42490  sge0val  42668  sge0tsms  42682  smflimsuplem1  43114  smflimsuplem2  43115  smflimsuplem4  43117