Theorem elpwi2 5292

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 5291	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 233	1 ⊢ 𝐴 ∈ 𝒫 𝐵

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3457  df-in 3912  df-ss 3922  df-pw 4558

This theorem is referenced by:  canth  7351  mptmpoopabbrd  8063  aceq3lem  10077  axdc3lem4  10411  uzf  12843  ixxf  13360  fzf  13517  bitsf  16462  prdsvallem  17484  prdsds  17494  wunnat  17993  ocvfval  21719  leordtval2  23273  cnpfval  23295  iscnp2  23300  islly2  23545  xkotf  23646  alexsubALTlem4  24111  sszcld  24879  bndth  25021  ishtpy  25035  fpwrelmap  32936  ballotlem2  34787  satfrnmapom  35721  cover2  38215  clsk1indlem1  44622  sprsymrelfolem1  48099