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

Syntax hints:   ∈ wcel 2143   ⊆ wss 3905  𝒫 cpw 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-pw 4564

This theorem is referenced by:  canth  7364  mptmpoopabbrd  8074  aceq3lem  10100  axdc3lem4  10432  uzf  12860  ixxf  13377  fzf  13534  bitsf  16480  prdsvallem  17502  prdsds  17512  wunnat  18011  ocvfval  21816  leordtval2  23369  cnpfval  23391  iscnp2  23396  islly2  23641  xkotf  23742  alexsubALTlem4  24207  sszcld  24975  bndth  25117  ishtpy  25131  fpwrelmap  33078  ballotlem2  34879  satfrnmapom  35862  cover2  38386  clsk1indlem1  44791  sprsymrelfolem1  48261