Theorem elpwd 4538

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  sselpwd  5245  pwel  5299  frd  5539  f1opw2  7502  pwuncl  7598  f1opwfi  9053  ackbij1lem6  9912  ackbij1lem11  9917  mreacs  17284  sylow3lem3  19149  sylow3lem6  19152  cmpcov  22448  tgqtop  22771  filss  22912  fnpreimac  30910  pcmplfin  31712  rspectopn  31719  zarclsint  31724  zarcmplem  31733  indval  31881  reprval  32490  scutval  33921  madecut  33992  cofcut1  34017  bj-sselpwuni  35150  bj-discrmoore  35209  dmvolss  43416  sge0xaddlem1  43861  meadjuni  43885  ovnval2b  43980  ovnsubadd2lem  44073  vonvolmbllem  44088  vonvolmbl  44089  smfresal  44209  smfpimbor1lem1  44219  sprsymrelfvlem  44830  lindslinindsimp1  45686  lindslinindimp2lem4  45690  lincresunit3  45710  iscnrm3llem1  46131