Theorem elpwi2 5346

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

Syntax hints:   ∈ wcel 2106   ⊆ wss 3948  𝒫 cpw 4602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  canth  7364  aceq3lem  10117  axdc3lem4  10450  uzf  12829  ixxf  13338  fzf  13492  bitsf  16372  prdsvallem  17404  prdsds  17414  wunnat  17911  wunnatOLD  17912  ocvfval  21438  leordtval2  22936  cnpfval  22958  iscnp2  22963  islly2  23208  xkotf  23309  alexsubALTlem4  23774  sszcld  24553  bndth  24698  ishtpy  24712  fpwrelmap  32213  ballotlem2  33773  satfrnmapom  34647  cover2  36886  clsk1indlem1  43098  sprsymrelfolem1  46459