Theorem elpwd 4557

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

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

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 3920  df-pw 4553

This theorem is referenced by:  sselpwd  5267  pwel  5320  frd  5576  f1opw2  7604  pwuncl  7706  naddunif  8611  f1opwfi  9246  ackbij1lem6  10118  ackbij1lem11  10123  mreacs  17564  sylow3lem3  19508  sylow3lem6  19511  cmpcov  23274  tgqtop  23597  filss  23738  scutval  27711  madecut  27797  cofcut1  27833  cutlt  27845  elons2d  28165  onscutlt  28170  bdayon  28178  fnpreimac  32614  indval  32796  exsslsb  33563  pcmplfin  33827  rspectopn  33834  zarclsint  33839  zarcmplem  33848  reprval  34578  bj-sselpwuni  37024  bj-discrmoore  37085  dmvolss  45966  sge0xaddlem1  46414  meadjuni  46438  ovnval2b  46533  ovnsubadd2lem  46626  vonvolmbllem  46641  vonvolmbl  46642  smfresal  46769  smfpimbor1lem1  46779  sprsymrelfvlem  47474  isubgruhgr  47852  grimuhgr  47871  gpgiedgdmellem  48030  lindslinindsimp1  48442  lindslinindimp2lem4  48446  lincresunit3  48466  iscnrm3llem1  48933