Theorem elpwd 4568

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2143   ⊆ wss 3905  𝒫 cpw 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-pw 4564

This theorem is referenced by:  pwidg  4582  sselpwd  5299  pwel  5352  frd  5618  f1opw2  7665  pwuncl  7765  naddunif  8676  f1opwfi  9309  ackbij1lem6  10203  ackbij1lem11  10208  indval  12216  mreacs  17709  sylow3lem3  19694  sylow3lem6  19697  cmpcov  23546  tgqtop  23869  filss  24010  nulsltsd  27970  nulsgtsd  27971  cutsval  27973  madecut  28076  cofcut1  28113  cutlt  28125  elons2d  28452  oncutlt  28457  bdayons  28469  fnpreimac  33015  exsslsb  33987  pcmplfin  34250  rspectopn  34257  zarclsint  34262  zarcmplem  34271  reprval  34997  bj-sselpwuni  37686  bj-discrmoore  37753  dmvolss  46699  sge0xaddlem1  47147  meadjuni  47171  ovnval2b  47266  ovnsubadd2lem  47359  vonvolmbllem  47374  vonvolmbl  47375  smfresal  47502  smfpimbor1lem1  47512  sprsymrelfvlem  48239  isubgruhgr  48633  grimuhgr  48652  gpgiedgdmellem  48811  lindslinindsimp1  49237  lindslinindimp2lem4  49241  lincresunit3  49261  iscnrm3llem1  49727