Theorem grusn

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

	Ref	Expression
Assertion	grusn	|- ( ( U e. Univ /\ A e. U ) -> { A } e. U )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	|- { A } = { A , A }
2		grupr	|- ( ( U e. Univ /\ A e. U /\ A e. U ) -> { A , A } e. U )
3	2	3anidm23	|- ( ( U e. Univ /\ A e. U ) -> { A , A } e. U )
4	1 3	eqeltrid	|- ( ( U e. Univ /\ A e. U ) -> { A } e. U )