Theorem elpwd 4606

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108   ⊆ wss 3951  𝒫 cpw 4600

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-pw 4602

This theorem is referenced by:  sselpwd  5328  pwel  5381  frd  5641  f1opw2  7688  pwuncl  7790  naddunif  8731  f1opwfi  9396  ackbij1lem6  10264  ackbij1lem11  10269  mreacs  17701  sylow3lem3  19647  sylow3lem6  19650  cmpcov  23397  tgqtop  23720  filss  23861  scutval  27845  madecut  27921  cofcut1  27954  cutlt  27966  elons2d  28282  fnpreimac  32681  indval  32838  exsslsb  33647  pcmplfin  33859  rspectopn  33866  zarclsint  33871  zarcmplem  33880  reprval  34625  bj-sselpwuni  37051  bj-discrmoore  37112  dmvolss  46000  sge0xaddlem1  46448  meadjuni  46472  ovnval2b  46567  ovnsubadd2lem  46660  vonvolmbllem  46675  vonvolmbl  46676  smfresal  46803  smfpimbor1lem1  46813  sprsymrelfvlem  47477  isubgruhgr  47854  grimuhgr  47878  gpgedgel  48007  lindslinindsimp1  48374  lindslinindimp2lem4  48378  lincresunit3  48398  iscnrm3llem1  48846