Theorem elpwd 4571

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106   ⊆ wss 3913  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  sselpwd  5288  pwel  5341  frd  5597  f1opw2  7613  pwuncl  7709  naddunif  8644  f1opwfi  9307  ackbij1lem6  10170  ackbij1lem11  10175  mreacs  17552  sylow3lem3  19425  sylow3lem6  19428  cmpcov  22777  tgqtop  23100  filss  23241  scutval  27182  madecut  27255  cofcut1  27282  fnpreimac  31654  pcmplfin  32530  rspectopn  32537  zarclsint  32542  zarcmplem  32551  indval  32701  reprval  33312  bj-sselpwuni  35594  bj-discrmoore  35655  dmvolss  44346  sge0xaddlem1  44794  meadjuni  44818  ovnval2b  44913  ovnsubadd2lem  45006  vonvolmbllem  45021  vonvolmbl  45022  smfresal  45149  smfpimbor1lem1  45159  sprsymrelfvlem  45802  lindslinindsimp1  46658  lindslinindimp2lem4  46662  lincresunit3  46682  iscnrm3llem1  47102