Theorem elpwd 4569

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

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

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 3931  df-pw 4565

This theorem is referenced by:  sselpwd  5283  pwel  5336  frd  5595  f1opw2  7644  pwuncl  7746  naddunif  8657  f1opwfi  9307  ackbij1lem6  10177  ackbij1lem11  10182  mreacs  17619  sylow3lem3  19559  sylow3lem6  19562  cmpcov  23276  tgqtop  23599  filss  23740  scutval  27712  madecut  27794  cofcut1  27828  cutlt  27840  elons2d  28160  onscutlt  28165  bdayon  28173  fnpreimac  32595  indval  32776  exsslsb  33592  pcmplfin  33850  rspectopn  33857  zarclsint  33862  zarcmplem  33871  reprval  34601  bj-sselpwuni  37038  bj-discrmoore  37099  dmvolss  45983  sge0xaddlem1  46431  meadjuni  46455  ovnval2b  46550  ovnsubadd2lem  46643  vonvolmbllem  46658  vonvolmbl  46659  smfresal  46786  smfpimbor1lem1  46796  sprsymrelfvlem  47491  isubgruhgr  47868  grimuhgr  47887  gpgiedgdmellem  48037  lindslinindsimp1  48446  lindslinindimp2lem4  48450  lincresunit3  48470  iscnrm3llem1  48937