Theorem elpwd 4611

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2106   ⊆ wss 3963  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-pw 4607

This theorem is referenced by:  sselpwd  5334  pwel  5387  frd  5645  f1opw2  7688  pwuncl  7789  naddunif  8730  f1opwfi  9394  ackbij1lem6  10262  ackbij1lem11  10267  mreacs  17703  sylow3lem3  19662  sylow3lem6  19665  cmpcov  23413  tgqtop  23736  filss  23877  scutval  27860  madecut  27936  cofcut1  27969  cutlt  27981  elons2d  28297  fnpreimac  32688  pcmplfin  33821  rspectopn  33828  zarclsint  33833  zarcmplem  33842  indval  33994  reprval  34604  bj-sselpwuni  37033  bj-discrmoore  37094  dmvolss  45941  sge0xaddlem1  46389  meadjuni  46413  ovnval2b  46508  ovnsubadd2lem  46601  vonvolmbllem  46616  vonvolmbl  46617  smfresal  46744  smfpimbor1lem1  46754  sprsymrelfvlem  47415  isubgruhgr  47792  grimuhgr  47816  gpgedgel  47943  lindslinindsimp1  48303  lindslinindimp2lem4  48307  lincresunit3  48327  iscnrm3llem1  48746