Theorem elpwi2 5301

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

This proof depends on syntax axioms:   ∈ wcel 2146   ⊆ wss 3900  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562

This theorem is used by:  canth  7384  mptmpoopabbrd  8105  aceq3lem  10212  axdc3lem4  10544  uzf  12981  ixxf  13499  fzf  13656  bitsf  16612  prdsvallem  17640  prdsds  17650  wunnat  18149  ocvfval  21987  leordtval2  23545  cnpfval  23567  iscnp2  23572  islly2  23818  xkotf  23919  alexsubALTlem4  24384  sszcld  25152  bndth  25294  ishtpy  25308  fpwrelmap  33381  ballotlem2  35177  satfrnmapom  36259  cover2  38792  clsk1indlem1  45188  sprsymrelfolem1  48716