Theorem elpwi2 5293

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3917  𝒫 cpw 4566

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  canth  7344  mptmpoopabbrd  8062  aceq3lem  10080  axdc3lem4  10413  uzf  12803  ixxf  13323  fzf  13479  bitsf  16404  prdsvallem  17424  prdsds  17434  wunnat  17928  ocvfval  21582  leordtval2  23106  cnpfval  23128  iscnp2  23133  islly2  23378  xkotf  23479  alexsubALTlem4  23944  sszcld  24713  bndth  24864  ishtpy  24878  fpwrelmap  32663  ballotlem2  34487  satfrnmapom  35364  cover2  37716  clsk1indlem1  44041  sprsymrelfolem1  47497