Theorem wunelss

Description: The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	|- ( ph -> U e. WUni )
	wununi.2	|- ( ph -> A e. U )
Assertion	wunelss	|- ( ph -> A C_ U )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	|- ( ph -> U e. WUni )
2		wununi.2	|- ( ph -> A e. U )
3		wuntr	|- ( U e. WUni -> Tr U )
4	1 3	syl	|- ( ph -> Tr U )
5		trss	|- ( Tr U -> ( A e. U -> A C_ U ) )
6	4 2 5	sylc	|- ( ph -> A C_ U )