Theorem elpwi2 5300

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

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899  𝒫 cpw 4557

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  canth  7368  mptmpoopabbrd  8081  aceq3lem  10126  axdc3lem4  10458  uzf  12893  ixxf  13411  fzf  13568  bitsf  16520  prdsvallem  17542  prdsds  17552  wunnat  18051  ocvfval  21882  leordtval2  23440  cnpfval  23462  iscnp2  23467  islly2  23713  xkotf  23814  alexsubALTlem4  24279  sszcld  25047  bndth  25189  ishtpy  25203  fpwrelmap  33207  ballotlem2  35003  satfrnmapom  35952  cover2  38468  clsk1indlem1  44888  sprsymrelfolem1  48395