Theorem gruss

Description: Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	gruss	|- ( ( U e. Univ /\ A e. U /\ B C_ A ) -> B e. U )

Proof

Step	Hyp	Ref	Expression
1		elpw2g	|- ( A e. U -> ( B e. ~P A <-> B C_ A ) )
2	1	adantl	|- ( ( U e. Univ /\ A e. U ) -> ( B e. ~P A <-> B C_ A ) )
3		grupw	|- ( ( U e. Univ /\ A e. U ) -> ~P A e. U )
4		gruelss	|- ( ( U e. Univ /\ ~P A e. U ) -> ~P A C_ U )
5	3 4	syldan	|- ( ( U e. Univ /\ A e. U ) -> ~P A C_ U )
6	5	sseld	|- ( ( U e. Univ /\ A e. U ) -> ( B e. ~P A -> B e. U ) )
7	2 6	sylbird	|- ( ( U e. Univ /\ A e. U ) -> ( B C_ A -> B e. U ) )
8	7	3impia	|- ( ( U e. Univ /\ A e. U /\ B C_ A ) -> B e. U )