Theorem elpwd 4547

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3889  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-pw 4543

This theorem is referenced by:  sselpwd  5269  pwel  5323  frd  5588  f1opw2  7622  pwuncl  7724  naddunif  8629  f1opwfi  9266  ackbij1lem6  10146  ackbij1lem11  10151  indval  12162  mreacs  17624  sylow3lem3  19604  sylow3lem6  19607  cmpcov  23354  tgqtop  23677  filss  23818  nulsltsd  27769  nulsgtsd  27770  cutsval  27772  madecut  27875  cofcut1  27912  cutlt  27924  elons2d  28251  oncutlt  28256  bdayons  28268  fnpreimac  32743  exsslsb  33741  pcmplfin  34004  rspectopn  34011  zarclsint  34016  zarcmplem  34025  reprval  34754  bj-sselpwuni  37357  bj-discrmoore  37423  dmvolss  46413  sge0xaddlem1  46861  meadjuni  46885  ovnval2b  46980  ovnsubadd2lem  47073  vonvolmbllem  47088  vonvolmbl  47089  smfresal  47216  smfpimbor1lem1  47226  sprsymrelfvlem  47950  isubgruhgr  48344  grimuhgr  48363  gpgiedgdmellem  48522  lindslinindsimp1  48933  lindslinindimp2lem4  48937  lincresunit3  48957  iscnrm3llem1  49424