Metamath Proof Explorer

Theorem gruelss

Description: A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 grutr 
 |-  ( U e. Univ -> Tr U )
2 trss 
 |-  ( Tr U -> ( A e. U -> A C_ U ) )
3 2 imp 
 |-  ( ( Tr U /\ A e. U ) -> A C_ U )
4 1 3 sylan 
 |-  ( ( U e. Univ /\ A e. U ) -> A C_ U )