Theorem wunss 10641

Description: A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
wununi.1	⊢ (𝜑 → 𝑈 ∈ WUni)
wununi.2	⊢ (𝜑 → 𝐴 ∈ 𝑈)
wunss.3	⊢ (𝜑 → 𝐵 ⊆ 𝐴)

Assertion

Ref	Expression
wunss	⊢ (𝜑 → 𝐵 ∈ 𝑈)

Proof of Theorem wunss

Step	Hyp	Ref	Expression
1		wununi.1	. . 3 ⊢ (𝜑 → 𝑈 ∈ WUni)
2		wununi.2	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
3	1, 2	wunpw 10636	. . 3 ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
4	1, 3	wunelss 10637	. 2 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝑈)
5		wunss.3	. . 3 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
6	2, 5	sselpwd 5278	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴)
7	4, 6	sseldd 3944	1 ⊢ (𝜑 → 𝐵 ∈ 𝑈)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911  𝒫 cpw 4559  WUnicwun 10629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561  df-uni 4868  df-tr 5210  df-wun 10631

This theorem is referenced by:  wunin  10642  wundif  10643  wunint  10644  wun0  10647  wunom  10649  wunxp  10653  wunpm  10654  wunmap  10655  wundm  10657  wunrn  10658  wuncnv  10659  wunres  10660  wunfv  10661  wunco  10662  wuntpos  10663  wuncn  11099  wunstr  17134  wunndx  17141  wunfunc  17839