Theorem elpwi2 5270

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)

Hypotheses

Ref	Expression
elpwi2.1	⊢ 𝐵 ∈ 𝑉
elpwi2.2	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
elpwi2	⊢ 𝐴 ∈ 𝒫 𝐵

Proof of Theorem elpwi2

Step	Hyp	Ref	Expression
1		elpwi2.2	. 2 ⊢ 𝐴 ⊆ 𝐵
2		elpwi2.1	. . . 4 ⊢ 𝐵 ∈ 𝑉
3	2	elexi 3451	. . 3 ⊢ 𝐵 ∈ V
4	3	elpw2 5269	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 230	1 ⊢ 𝐴 ∈ 𝒫 𝐵

Syntax hints:   ∈ wcel 2106   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  canth  7229  aceq3lem  9876  axdc3lem4  10209  uzf  12585  ixxf  13089  fzf  13243  bitsf  16134  prdsvallem  17165  prdsds  17175  wunnat  17672  wunnatOLD  17673  ocvfval  20871  leordtval2  22363  cnpfval  22385  iscnp2  22390  islly2  22635  xkotf  22736  alexsubALTlem4  23201  sszcld  23980  bndth  24121  ishtpy  24135  fpwrelmap  31068  ballotlem2  32455  satfrnmapom  33332  cover2  35872  clsk1indlem1  41655  sprsymrelfolem1  44944