Theorem gruuni

Description: A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013)

	Ref	Expression
Assertion	gruuni	|- ( ( U e. Univ /\ A e. U ) -> U. A e. U )

Proof

Step	Hyp	Ref	Expression
1		uniiun	|- U. A = U_ x e. A x
2		gruelss	|- ( ( U e. Univ /\ A e. U ) -> A C_ U )
3		dfss3	|- ( A C_ U <-> A. x e. A x e. U )
4	2 3	sylib	|- ( ( U e. Univ /\ A e. U ) -> A. x e. A x e. U )
5		gruiun	|- ( ( U e. Univ /\ A e. U /\ A. x e. A x e. U ) -> U_ x e. A x e. U )
6	4 5	mpd3an3	|- ( ( U e. Univ /\ A e. U ) -> U_ x e. A x e. U )
7	1 6	eqeltrid	|- ( ( U e. Univ /\ A e. U ) -> U. A e. U )