Theorem elpwd 4521

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Hypotheses

Ref	Expression
elpwd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
elpwd.2	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
elpwd	⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Proof of Theorem elpwd

Step	Hyp	Ref	Expression
1		elpwd.2	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		elpwd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		elpwg 4516	. . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	2, 3	syl 17	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
5	1, 4	mpbird 260	1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2110   ⊆ wss 3866  𝒫 cpw 4513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-pw 4515

This theorem is referenced by:  sselpwd  5219  pwel  5274  f1opw2  7460  pwuncl  7555  f1opwfi  8980  ackbij1lem6  9839  ackbij1lem11  9844  mreacs  17161  sylow3lem3  19018  sylow3lem6  19021  cmpcov  22286  tgqtop  22609  filss  22750  fnpreimac  30728  pcmplfin  31524  rspectopn  31531  zarclsint  31536  zarcmplem  31545  indval  31693  reprval  32302  scutval  33731  madecut  33802  cofcut1  33827  bj-sselpwuni  34960  bj-discrmoore  35017  dmvolss  43201  sge0xaddlem1  43646  meadjuni  43670  ovnval2b  43765  ovnsubadd2lem  43858  vonvolmbllem  43873  vonvolmbl  43874  smfresal  43994  smfpimbor1lem1  44004  sprsymrelfvlem  44615  lindslinindsimp1  45471  lindslinindimp2lem4  45475  lincresunit3  45495  iscnrm3llem1  45916