Theorem elpwi2 5101

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

Syntax hints:   ↔ wb 198   ∈ wcel 2051   ⊆ wss 3822  𝒫 cpw 4416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743  ax-sep 5056

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-v 3410  df-in 3829  df-ss 3836  df-pw 4418

This theorem is referenced by:  canth  6932  aceq3lem  9338  axdc3lem4  9671  uzf  12059  ixxf  12562  fzf  12710  bitsf  15634  prdsval  16582  prdsds  16591  wunnat  17096  ocvfval  20527  leordtval2  21539  cnpfval  21561  iscnp2  21566  islly2  21811  xkotf  21912  alexsubALTlem4  22377  sszcld  23143  bndth  23280  ishtpy  23294  ballotlem2  31424  cover2  34468  sprsymrelfolem1  43056