Theorem unimax

Description: Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002)

	Ref	Expression
Assertion	unimax	|- ( A e. B -> U. { x e. B | x C_ A } = A )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- A C_ A
2		sseq1	|- ( x = A -> ( x C_ A <-> A C_ A ) )
3	2	elrab3	|- ( A e. B -> ( A e. { x e. B | x C_ A } <-> A C_ A ) )
4	1 3	mpbiri	|- ( A e. B -> A e. { x e. B | x C_ A } )
5		sseq1	|- ( x = y -> ( x C_ A <-> y C_ A ) )
6	5	elrab	|- ( y e. { x e. B | x C_ A } <-> ( y e. B /\ y C_ A ) )
7	6	simprbi	|- ( y e. { x e. B | x C_ A } -> y C_ A )
8	7	rgen	|- A. y e. { x e. B | x C_ A } y C_ A
9		ssunieq	|- ( ( A e. { x e. B | x C_ A } /\ A. y e. { x e. B | x C_ A } y C_ A ) -> A = U. { x e. B | x C_ A } )
10	9	eqcomd	|- ( ( A e. { x e. B | x C_ A } /\ A. y e. { x e. B | x C_ A } y C_ A ) -> U. { x e. B | x C_ A } = A )
11	4 8 10	sylancl	|- ( A e. B -> U. { x e. B | x C_ A } = A )