Theorem elpwd 4562

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2144   ⊆ wss 3896  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897  df-pw 4558

This theorem is used by:  pwidg  4577  sselpwd  5290  pwel  5343  frd  5608  f1opw2  7680  pwuncl  7788  naddunif  8710  f1opwfi  9352  ackbij1lem6  10309  ackbij1lem11  10314  indval  12330  mreacs  17841  sylow3lem3  19852  sylow3lem6  19855  cmpcov  23716  tgqtop  24040  filss  24181  nulsltsd  28172  nulsgtsd  28173  cutsval  28175  madecut  28278  cofcut1  28315  cutlt  28327  elons2d  28654  oncutlt  28659  bdayons  28671  fnpreimac  33315  exsslsb  34279  cmpcref  34532  pcmplfin  34542  rspectopn  34549  zarclsint  34554  zarcmplem  34563  omssubadd  34982  reprval  35289  bj-sselpwuni  38073  bj-discrmoore  38140  ishfstruct  46136  dmvolss  47103  sge0xaddlem1  47551  meadjuni  47575  ovnval2b  47670  ovnsubadd2lem  47763  vonvolmbllem  47778  vonvolmbl  47779  smfresal  47906  smfpimbor1lem1  47916  sprsymrelfvlem  48680  isubgruhgr  49074  grimuhgr  49093  gpgiedgdmellem  49252  lindslinindsimp1  49677  lindslinindimp2lem4  49681  lincresunit3  49701  iscnrm3llem1  50171