Theorem elpwd 4565

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3911  𝒫 cpw 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-pw 4561

This theorem is referenced by:  sselpwd  5278  pwel  5331  frd  5588  f1opw2  7624  pwuncl  7726  naddunif  8634  f1opwfi  9283  ackbij1lem6  10153  ackbij1lem11  10158  mreacs  17595  sylow3lem3  19535  sylow3lem6  19538  cmpcov  23252  tgqtop  23575  filss  23716  scutval  27688  madecut  27770  cofcut1  27804  cutlt  27816  elons2d  28136  onscutlt  28141  bdayon  28149  fnpreimac  32568  indval  32749  exsslsb  33565  pcmplfin  33823  rspectopn  33830  zarclsint  33835  zarcmplem  33844  reprval  34574  bj-sselpwuni  37011  bj-discrmoore  37072  dmvolss  45956  sge0xaddlem1  46404  meadjuni  46428  ovnval2b  46523  ovnsubadd2lem  46616  vonvolmbllem  46631  vonvolmbl  46632  smfresal  46759  smfpimbor1lem1  46769  sprsymrelfvlem  47464  isubgruhgr  47841  grimuhgr  47860  gpgiedgdmellem  48010  lindslinindsimp1  48419  lindslinindimp2lem4  48423  lincresunit3  48443  iscnrm3llem1  48910