Theorem elpwd 4561

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2142   ⊆ wss 3904  𝒫 cpw 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-pw 4557

This theorem is referenced by:  pwidg  4575  sselpwd  5284  pwel  5338  frd  5604  f1opw2  7651  pwuncl  7753  naddunif  8664  f1opwfi  9299  ackbij1lem6  10180  ackbij1lem11  10185  indval  12198  mreacs  17690  sylow3lem3  19669  sylow3lem6  19672  cmpcov  23446  tgqtop  23769  filss  23910  nulsltsd  27867  nulsgtsd  27868  cutsval  27870  madecut  27973  cofcut1  28010  cutlt  28022  elons2d  28349  oncutlt  28354  bdayons  28366  fnpreimac  32869  exsslsb  33891  pcmplfin  34154  rspectopn  34161  zarclsint  34166  zarcmplem  34175  reprval  34901  bj-sselpwuni  37532  bj-discrmoore  37598  dmvolss  46556  sge0xaddlem1  47004  meadjuni  47028  ovnval2b  47123  ovnsubadd2lem  47216  vonvolmbllem  47231  vonvolmbl  47232  smfresal  47359  smfpimbor1lem1  47369  sprsymrelfvlem  48093  isubgruhgr  48487  grimuhgr  48506  gpgiedgdmellem  48665  lindslinindsimp1  49076  lindslinindimp2lem4  49080  lincresunit3  49100  iscnrm3llem1  49567