Theorem elpwi2 5280

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3901  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  canth  7312  mptmpoopabbrd  8024  aceq3lem  10032  axdc3lem4  10365  uzf  12756  ixxf  13273  fzf  13429  bitsf  16356  prdsvallem  17376  prdsds  17386  wunnat  17885  ocvfval  21623  leordtval2  23158  cnpfval  23180  iscnp2  23185  islly2  23430  xkotf  23531  alexsubALTlem4  23996  sszcld  24764  bndth  24915  ishtpy  24929  fpwrelmap  32814  ballotlem2  34648  satfrnmapom  35566  cover2  37918  clsk1indlem1  44307  sprsymrelfolem1  47759