Theorem elpwi2 5306

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

Syntax hints:   ∈ wcel 2149   ⊆ wss 3913  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-pw 4569

This theorem is referenced by:  canth  7365  mptmpoopabbrd  8078  aceq3lem  10104  axdc3lem4  10437  uzf  12865  ixxf  13382  fzf  13539  bitsf  16485  prdsvallem  17507  prdsds  17517  wunnat  18016  ocvfval  21785  leordtval2  23338  cnpfval  23360  iscnp2  23365  islly2  23610  xkotf  23711  alexsubALTlem4  24176  sszcld  24944  bndth  25086  ishtpy  25100  fpwrelmap  33019  ballotlem2  34824  satfrnmapom  35795  cover2  38288  clsk1indlem1  44697  sprsymrelfolem1  48164