Theorem elpwi2 5278

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3899  𝒫 cpw 4552

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-pw 4554

This theorem is referenced by:  canth  7310  mptmpoopabbrd  8022  aceq3lem  10028  axdc3lem4  10361  uzf  12752  ixxf  13269  fzf  13425  bitsf  16352  prdsvallem  17372  prdsds  17382  wunnat  17881  ocvfval  21619  leordtval2  23154  cnpfval  23176  iscnp2  23181  islly2  23426  xkotf  23527  alexsubALTlem4  23992  sszcld  24760  bndth  24911  ishtpy  24925  fpwrelmap  32761  ballotlem2  34595  satfrnmapom  35513  cover2  37855  clsk1indlem1  44228  sprsymrelfolem1  47680