Theorem elpwi2 5290

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  canth  7341  mptmpoopabbrd  8059  aceq3lem  10073  axdc3lem4  10406  uzf  12796  ixxf  13316  fzf  13472  bitsf  16397  prdsvallem  17417  prdsds  17427  wunnat  17921  ocvfval  21575  leordtval2  23099  cnpfval  23121  iscnp2  23126  islly2  23371  xkotf  23472  alexsubALTlem4  23937  sszcld  24706  bndth  24857  ishtpy  24871  fpwrelmap  32656  ballotlem2  34480  satfrnmapom  35357  cover2  37709  clsk1indlem1  44034  sprsymrelfolem1  47493