Theorem elpwd 4541

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  sselpwd  5250  pwel  5304  frd  5548  f1opw2  7524  pwuncl  7620  f1opwfi  9123  ackbij1lem6  9981  ackbij1lem11  9986  mreacs  17367  sylow3lem3  19234  sylow3lem6  19237  cmpcov  22540  tgqtop  22863  filss  23004  fnpreimac  31008  pcmplfin  31810  rspectopn  31817  zarclsint  31822  zarcmplem  31831  indval  31981  reprval  32590  scutval  33994  madecut  34065  cofcut1  34090  bj-sselpwuni  35223  bj-discrmoore  35282  dmvolss  43526  sge0xaddlem1  43971  meadjuni  43995  ovnval2b  44090  ovnsubadd2lem  44183  vonvolmbllem  44198  vonvolmbl  44199  smfresal  44322  smfpimbor1lem1  44332  sprsymrelfvlem  44942  lindslinindsimp1  45798  lindslinindimp2lem4  45802  lincresunit3  45822  iscnrm3llem1  46243