Theorem elpwi2 5264

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

Syntax hints:   ∈ wcel 2119   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5219

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  canth  7311  mptmpoopabbrd  8023  aceq3lem  10034  axdc3lem4  10367  uzf  12783  ixxf  13300  fzf  13457  bitsf  16388  prdsvallem  17409  prdsds  17419  wunnat  17918  ocvfval  21642  leordtval2  23196  cnpfval  23218  iscnp2  23223  islly2  23468  xkotf  23569  alexsubALTlem4  24034  sszcld  24802  bndth  24944  ishtpy  24958  fpwrelmap  32826  ballotlem2  34682  satfrnmapom  35607  cover2  38091  clsk1indlem1  44498  sprsymrelfolem1  47975