Theorem elpwi2 5305

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

This proof depends on syntax axioms:   ∈ wcel 2142   ⊆ wss 3904  𝒫 cpw 4561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-pw 4563

This theorem is used by:  canth  7366  mptmpoopabbrd  8076  aceq3lem  10111  axdc3lem4  10443  uzf  12871  ixxf  13388  fzf  13545  bitsf  16491  prdsvallem  17513  prdsds  17523  wunnat  18022  ocvfval  21827  leordtval2  23380  cnpfval  23402  iscnp2  23407  islly2  23652  xkotf  23753  alexsubALTlem4  24218  sszcld  24986  bndth  25128  ishtpy  25142  fpwrelmap  33089  ballotlem2  34888  satfrnmapom  35870  cover2  38394  clsk1indlem1  44799  sprsymrelfolem1  48269