Theorem elpwi2 5274

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3903  𝒫 cpw 4551

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553

This theorem is referenced by:  canth  7303  mptmpoopabbrd  8015  aceq3lem  10014  axdc3lem4  10347  uzf  12738  ixxf  13258  fzf  13414  bitsf  16338  prdsvallem  17358  prdsds  17368  wunnat  17866  ocvfval  21573  leordtval2  23097  cnpfval  23119  iscnp2  23124  islly2  23369  xkotf  23470  alexsubALTlem4  23935  sszcld  24704  bndth  24855  ishtpy  24869  fpwrelmap  32677  ballotlem2  34463  satfrnmapom  35353  cover2  37705  clsk1indlem1  44028  sprsymrelfolem1  47486