Theorem elpwi2 5265

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 3441	. . 3 ⊢ 𝐵 ∈ V
4	3	elpw2 5264	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 230	1 ⊢ 𝐴 ∈ 𝒫 𝐵

Syntax hints:   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  canth  7209  aceq3lem  9807  axdc3lem4  10140  uzf  12514  ixxf  13018  fzf  13172  bitsf  16062  prdsvallem  17082  prdsds  17092  wunnat  17588  wunnatOLD  17589  ocvfval  20783  leordtval2  22271  cnpfval  22293  iscnp2  22298  islly2  22543  xkotf  22644  alexsubALTlem4  23109  sszcld  23886  bndth  24027  ishtpy  24041  fpwrelmap  30970  ballotlem2  32355  satfrnmapom  33232  cover2  35799  clsk1indlem1  41544  sprsymrelfolem1  44832