Theorem elpwi2 5308

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

This proof depends on syntax axioms:   ∈ wcel 2146   ⊆ wss 3906  𝒫 cpw 4564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-pw 4566

This theorem is used by:  canth  7373  mptmpoopabbrd  8084  aceq3lem  10120  axdc3lem4  10452  uzf  12883  ixxf  13400  fzf  13557  bitsf  16509  prdsvallem  17531  prdsds  17541  wunnat  18040  ocvfval  21868  leordtval2  23421  cnpfval  23443  iscnp2  23448  islly2  23694  xkotf  23795  alexsubALTlem4  24260  sszcld  25028  bndth  25170  ishtpy  25184  fpwrelmap  33150  ballotlem2  34946  satfrnmapom  35901  cover2  38426  clsk1indlem1  44831  sprsymrelfolem1  48301