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  17599  sylow3lem3  19543  sylow3lem6  19546  cmpcov  23309  tgqtop  23632  filss  23773  scutval  27746  madecut  27832  cofcut1  27868  cutlt  27880  elons2d  28200  onscutlt  28205  bdayon  28213  fnpreimac  32645  indval  32826  exsslsb  33585  pcmplfin  33843  rspectopn  33850  zarclsint  33855  zarcmplem  33864  reprval  34594  bj-sselpwuni  37031  bj-discrmoore  37092  dmvolss  45976  sge0xaddlem1  46424  meadjuni  46448  ovnval2b  46543  ovnsubadd2lem  46636  vonvolmbllem  46651  vonvolmbl  46652  smfresal  46779  smfpimbor1lem1  46789  sprsymrelfvlem  47484  isubgruhgr  47861  grimuhgr  47880  gpgiedgdmellem  48030  lindslinindsimp1  48439  lindslinindimp2lem4  48443  lincresunit3  48463  iscnrm3llem1  48930