Theorem ssintub

Description: Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000)

	Ref	Expression
Assertion	ssintub	|- A C_ |^| { x e. B | A C_ x }

Proof

Step	Hyp	Ref	Expression
1		ssint	|- ( A C_ |^| { x e. B | A C_ x } <-> A. y e. { x e. B | A C_ x } A C_ y )
2		sseq2	|- ( x = y -> ( A C_ x <-> A C_ y ) )
3	2	elrab	|- ( y e. { x e. B | A C_ x } <-> ( y e. B /\ A C_ y ) )
4	3	simprbi	|- ( y e. { x e. B | A C_ x } -> A C_ y )
5	1 4	mprgbir	|- A C_ |^| { x e. B | A C_ x }