Theorem elpwi2 5353

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  canth  7401  mptmpoopabbrd  8121  aceq3lem  10189  axdc3lem4  10522  uzf  12906  ixxf  13417  fzf  13571  bitsf  16473  prdsvallem  17514  prdsds  17524  wunnat  18024  wunnatOLD  18025  ocvfval  21707  leordtval2  23241  cnpfval  23263  iscnp2  23268  islly2  23513  xkotf  23614  alexsubALTlem4  24079  sszcld  24858  bndth  25009  ishtpy  25023  fpwrelmap  32747  ballotlem2  34453  satfrnmapom  35338  cover2  37675  clsk1indlem1  44007  sprsymrelfolem1  47366