Theorem elpwi2 5297

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

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  canth  7374  mptmpoopabbrd  8094  aceq3lem  10199  axdc3lem4  10531  uzf  12968  ixxf  13486  fzf  13643  bitsf  16597  prdsvallem  17625  prdsds  17635  wunnat  18134  ocvfval  21972  leordtval2  23530  cnpfval  23552  iscnp2  23557  islly2  23803  xkotf  23904  alexsubALTlem4  24369  sszcld  25137  bndth  25279  ishtpy  25293  fpwrelmap  33325  ballotlem2  35121  satfrnmapom  36135  cover2  38649  clsk1indlem1  45044  sprsymrelfolem1  48573