Theorem elpwi2 5283

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

Syntax hints:   ∈ wcel 2105   ⊆ wss 3896  𝒫 cpw 4543

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5236

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3443  df-in 3903  df-ss 3913  df-pw 4545

This theorem is referenced by:  canth  7267  aceq3lem  9946  axdc3lem4  10279  uzf  12655  ixxf  13159  fzf  13313  bitsf  16203  prdsvallem  17232  prdsds  17242  wunnat  17739  wunnatOLD  17740  ocvfval  20942  leordtval2  22434  cnpfval  22456  iscnp2  22461  islly2  22706  xkotf  22807  alexsubALTlem4  23272  sszcld  24051  bndth  24192  ishtpy  24206  fpwrelmap  31176  ballotlem2  32561  satfrnmapom  33438  cover2  35932  clsk1indlem1  41883  sprsymrelfolem1  45203