Theorem elpwi2 5305

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3926  𝒫 cpw 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  canth  7359  mptmpoopabbrd  8079  aceq3lem  10134  axdc3lem4  10467  uzf  12855  ixxf  13372  fzf  13528  bitsf  16446  prdsvallem  17468  prdsds  17478  wunnat  17972  ocvfval  21626  leordtval2  23150  cnpfval  23172  iscnp2  23177  islly2  23422  xkotf  23523  alexsubALTlem4  23988  sszcld  24757  bndth  24908  ishtpy  24922  fpwrelmap  32710  ballotlem2  34521  satfrnmapom  35392  cover2  37739  clsk1indlem1  44069  sprsymrelfolem1  47506