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 2732

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

This theorem is used by:  pwidg  4577  sselpwd  5293  pwel  5346  frd  5612  f1opw2  7669  pwuncl  7769  naddunif  8682  f1opwfi  9323  ackbij1lem6  10226  ackbij1lem11  10231  indval  12245  mreacs  17746  sylow3lem3  19756  sylow3lem6  19759  cmpcov  23614  tgqtop  23938  filss  24079  nulsltsd  28042  nulsgtsd  28043  cutsval  28045  madecut  28148  cofcut1  28185  cutlt  28197  elons2d  28524  oncutlt  28529  bdayons  28541  fnpreimac  33143  exsslsb  34107  pcmplfin  34370  rspectopn  34377  zarclsint  34382  zarcmplem  34391  reprval  35118  bj-sselpwuni  37794  bj-discrmoore  37861  dmvolss  46813  sge0xaddlem1  47261  meadjuni  47285  ovnval2b  47380  ovnsubadd2lem  47473  vonvolmbllem  47488  vonvolmbl  47489  smfresal  47616  smfpimbor1lem1  47626  sprsymrelfvlem  48390  isubgruhgr  48784  grimuhgr  48803  gpgiedgdmellem  48962  lindslinindsimp1  49387  lindslinindimp2lem4  49391  lincresunit3  49411  iscnrm3llem1  49875