Theorem wunss 9413

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 9408	. . 3 ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
4	1, 3	wunelss 9409	. 2 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝑈)
5		wunss.3	. . 3 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
6		elpw2g 4754	. . . 4 ⊢ (𝐴 ∈ 𝑈 → (𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴))
7	2, 6	syl 17	. . 3 ⊢ (𝜑 → (𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴))
8	5, 7	mpbird 246	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴)
9	4, 8	sseldd 3569	1 ⊢ (𝜑 → 𝐵 ∈ 𝑈)

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108  WUnicwun 9401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373  df-tr 4681  df-wun 9403

This theorem is referenced by:  wunin  9414  wundif  9415  wunint  9416  wun0  9419  wunom  9421  wunxp  9425  wunpm  9426  wunmap  9427  wundm  9429  wunrn  9430  wuncnv  9431  wunres  9432  wunfv  9433  wunco  9434  wuntpos  9435  wuncn  9870  wunndx  15711  wunstr  15714  wunfunc  16382