Metamath Proof Explorer

Theorem gruel

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

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

Proof

Step Hyp Ref Expression
1 gruelss 
 |-  ( ( U e. Univ /\ A e. U ) -> A C_ U )
2 1 sseld 
 |-  ( ( U e. Univ /\ A e. U ) -> ( B e. A -> B e. U ) )
3 2 3impia 
 |-  ( ( U e. Univ /\ A e. U /\ B e. A ) -> B e. U )