Theorem wunss 10626

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 10621	. . 3 ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
4	1, 3	wunelss 10622	. 2 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝑈)
5		wunss.3	. . 3 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
6	2, 5	sselpwd 5256	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴)
7	4, 6	sseldd 3916	1 ⊢ (𝜑 → 𝐵 ∈ 𝑈)

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883  𝒫 cpw 4529  WUnicwun 10614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4531  df-uni 4839  df-tr 5180  df-wun 10616

This theorem is referenced by:  wunin  10627  wundif  10628  wunint  10629  wun0  10632  wunom  10634  wunxp  10638  wunpm  10639  wunmap  10640  wundm  10642  wunrn  10643  wuncnv  10644  wunres  10645  wunfv  10646  wunco  10647  wuntpos  10648  wuncn  11084  wunstr  17149  wunndx  17156  wunfunc  17859