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

Metamath Proof Explorer

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 )