This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supex

Description: A supremum is a set. (Contributed by NM, 22-May-1999)

Ref Expression
Hypothesis supex.1 ⊢ R Or A
Assertion supex ⊢ sup B A R ∈ V

Proof

Step Hyp Ref Expression
1 supex.1 ⊢ R Or A
2 id ⊢ R Or A → R Or A
3 2 supexd ⊢ R Or A → sup B A R ∈ V
4 1 3 ax-mp ⊢ sup B A R ∈ V