Theorem elpwd 4563

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-pw 4559

This theorem is used by:  pwidg  4577  sselpwd  5290  pwel  5343  frd  5608  f1opw2  7676  pwuncl  7784  naddunif  8703  f1opwfi  9345  ackbij1lem6  10302  ackbij1lem11  10307  indval  12323  mreacs  17832  sylow3lem3  19843  sylow3lem6  19846  cmpcov  23707  tgqtop  24031  filss  24172  nulsltsd  28163  nulsgtsd  28164  cutsval  28166  madecut  28269  cofcut1  28306  cutlt  28318  elons2d  28645  oncutlt  28650  bdayons  28662  fnpreimac  33264  exsslsb  34229  pcmplfin  34492  rspectopn  34499  zarclsint  34504  zarcmplem  34513  reprval  35239  bj-sselpwuni  37965  bj-discrmoore  38032  ishfstruct  46028  dmvolss  46995  sge0xaddlem1  47443  meadjuni  47467  ovnval2b  47562  ovnsubadd2lem  47655  vonvolmbllem  47670  vonvolmbl  47671  smfresal  47798  smfpimbor1lem1  47808  sprsymrelfvlem  48572  isubgruhgr  48966  grimuhgr  48985  gpgiedgdmellem  49144  lindslinindsimp1  49569  lindslinindimp2lem4  49573  lincresunit3  49593  iscnrm3llem1  50057