This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )