Theorem elpwi2 5282

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  canth  7322  mptmpoopabbrd  8034  aceq3lem  10042  axdc3lem4  10375  uzf  12766  ixxf  13283  fzf  13439  bitsf  16366  prdsvallem  17386  prdsds  17396  wunnat  17895  ocvfval  21636  leordtval2  23171  cnpfval  23193  iscnp2  23198  islly2  23443  xkotf  23544  alexsubALTlem4  24009  sszcld  24777  bndth  24928  ishtpy  24942  fpwrelmap  32827  ballotlem2  34671  satfrnmapom  35590  cover2  37970  clsk1indlem1  44405  sprsymrelfolem1  47856