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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-pw 4558

This theorem is referenced by:  sselpwd  5275  pwel  5328  frd  5589  f1opw2  7623  pwuncl  7725  naddunif  8631  f1opwfi  9268  ackbij1lem6  10146  ackbij1lem11  10151  mreacs  17593  sylow3lem3  19570  sylow3lem6  19573  cmpcov  23345  tgqtop  23668  filss  23809  nulsltsd  27785  nulsgtsd  27786  cutsval  27788  madecut  27891  cofcut1  27928  cutlt  27940  elons2d  28267  oncutlt  28272  bdayons  28284  fnpreimac  32760  indval  32943  exsslsb  33774  pcmplfin  34038  rspectopn  34045  zarclsint  34050  zarcmplem  34059  reprval  34788  bj-sselpwuni  37298  bj-discrmoore  37364  dmvolss  46343  sge0xaddlem1  46791  meadjuni  46815  ovnval2b  46910  ovnsubadd2lem  47003  vonvolmbllem  47018  vonvolmbl  47019  smfresal  47146  smfpimbor1lem1  47156  sprsymrelfvlem  47850  isubgruhgr  48228  grimuhgr  48247  gpgiedgdmellem  48406  lindslinindsimp1  48817  lindslinindimp2lem4  48821  lincresunit3  48841  iscnrm3llem1  49308