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 ) e. _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 ) e. _V )
4	1 3	ax-mp	|- sup ( B , A , R ) e. _V