Theorem elpwi2 5224

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

Syntax hints:   ∈ wcel 2112   ⊆ wss 3853  𝒫 cpw 4499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870  df-pw 4501

This theorem is referenced by:  canth  7145  aceq3lem  9699  axdc3lem4  10032  uzf  12406  ixxf  12910  fzf  13064  bitsf  15949  prdsvallem  16913  prdsds  16923  wunnat  17417  wunnatOLD  17418  ocvfval  20582  leordtval2  22063  cnpfval  22085  iscnp2  22090  islly2  22335  xkotf  22436  alexsubALTlem4  22901  sszcld  23668  bndth  23809  ishtpy  23823  fpwrelmap  30742  ballotlem2  32121  satfrnmapom  32999  cover2  35558  clsk1indlem1  41273  sprsymrelfolem1  44560