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	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	wunelss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		wuntr	⊢ ( 𝑈 ∈ WUni → Tr 𝑈 )
4	1 3	syl	⊢ ( 𝜑 → Tr 𝑈 )
5		trss	⊢ ( Tr 𝑈 → ( 𝐴 ∈ 𝑈 → 𝐴 ⊆ 𝑈 ) )
6	4 2 5	sylc	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )