Theorem elpwi2 5285

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3911  𝒫 cpw 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  canth  7323  mptmpoopabbrd  8038  aceq3lem  10049  axdc3lem4  10382  uzf  12772  ixxf  13292  fzf  13448  bitsf  16373  prdsvallem  17393  prdsds  17403  wunnat  17901  ocvfval  21608  leordtval2  23132  cnpfval  23154  iscnp2  23159  islly2  23404  xkotf  23505  alexsubALTlem4  23970  sszcld  24739  bndth  24890  ishtpy  24904  fpwrelmap  32706  ballotlem2  34473  satfrnmapom  35350  cover2  37702  clsk1indlem1  44027  sprsymrelfolem1  47486