Theorem elpwd 4560

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 4557	. . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
4	2, 3	syl 17	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113   ⊆ wss 3901  𝒫 cpw 4554

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-pw 4556

This theorem is referenced by:  sselpwd  5273  pwel  5326  frd  5581  f1opw2  7613  pwuncl  7715  naddunif  8621  f1opwfi  9256  ackbij1lem6  10134  ackbij1lem11  10139  mreacs  17581  sylow3lem3  19558  sylow3lem6  19561  cmpcov  23333  tgqtop  23656  filss  23797  nulsltsd  27773  nulsgtsd  27774  cutsval  27776  madecut  27879  cofcut1  27916  cutlt  27928  elons2d  28255  oncutlt  28260  bdayons  28272  fnpreimac  32749  indval  32932  exsslsb  33753  pcmplfin  34017  rspectopn  34024  zarclsint  34029  zarcmplem  34038  reprval  34767  bj-sselpwuni  37251  bj-discrmoore  37316  dmvolss  46229  sge0xaddlem1  46677  meadjuni  46701  ovnval2b  46796  ovnsubadd2lem  46889  vonvolmbllem  46904  vonvolmbl  46905  smfresal  47032  smfpimbor1lem1  47042  sprsymrelfvlem  47736  isubgruhgr  48114  grimuhgr  48133  gpgiedgdmellem  48292  lindslinindsimp1  48703  lindslinindimp2lem4  48707  lincresunit3  48727  iscnrm3llem1  49194