Theorem elpwi2 5251

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

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	. . 3 ⊢ 𝐵 ∈ 𝑉
3		elpw2g 5249	. . 3 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	2, 3	ax-mp 5	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 233	1 ⊢ 𝐴 ∈ 𝒫 𝐵

Syntax hints:   ↔ wb 208   ∈ wcel 2114   ⊆ wss 3938  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  canth  7113  aceq3lem  9548  axdc3lem4  9877  uzf  12249  ixxf  12751  fzf  12899  bitsf  15778  prdsval  16730  prdsds  16739  wunnat  17228  ocvfval  20812  leordtval2  21822  cnpfval  21844  iscnp2  21849  islly2  22094  xkotf  22195  alexsubALTlem4  22660  sszcld  23427  bndth  23564  ishtpy  23578  fpwrelmap  30471  ballotlem2  31748  satfrnmapom  32619  cover2  34991  clsk1indlem1  40402  sprsymrelfolem1  43661