Theorem wunss 10718

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 10713	. . 3 ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
4	1, 3	wunelss 10714	. 2 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝑈)
5		wunss.3	. . 3 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
6	2, 5	sselpwd 5295	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴)
7	4, 6	sseldd 3957	1 ⊢ (𝜑 → 𝐵 ∈ 𝑈)

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3924  𝒫 cpw 4573  WUnicwun 10706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5263

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-in 3931  df-ss 3941  df-pw 4575  df-uni 4881  df-tr 5227  df-wun 10708

This theorem is referenced by:  wunin  10719  wundif  10720  wunint  10721  wun0  10724  wunom  10726  wunxp  10730  wunpm  10731  wunmap  10732  wundm  10734  wunrn  10735  wuncnv  10736  wunres  10737  wunfv  10738  wunco  10739  wuntpos  10740  wuncn  11176  wunstr  17192  wunndx  17199  wunfunc  17899