Theorem elpwd 4535

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

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119   ⊆ wss 3883  𝒫 cpw 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-pw 4531

This theorem is referenced by:  sselpwd  5256  pwel  5310  frd  5575  f1opw2  7611  pwuncl  7713  naddunif  8619  f1opwfi  9256  ackbij1lem6  10137  ackbij1lem11  10142  indval  12153  mreacs  17615  sylow3lem3  19595  sylow3lem6  19598  cmpcov  23372  tgqtop  23695  filss  23836  nulsltsd  27787  nulsgtsd  27788  cutsval  27790  madecut  27893  cofcut1  27930  cutlt  27942  elons2d  28269  oncutlt  28274  bdayons  28286  fnpreimac  32762  exsslsb  33781  pcmplfin  34044  rspectopn  34051  zarclsint  34056  zarcmplem  34065  reprval  34794  bj-sselpwuni  37403  bj-discrmoore  37469  dmvolss  46428  sge0xaddlem1  46876  meadjuni  46900  ovnval2b  46995  ovnsubadd2lem  47088  vonvolmbllem  47103  vonvolmbl  47104  smfresal  47231  smfpimbor1lem1  47241  sprsymrelfvlem  47965  isubgruhgr  48359  grimuhgr  48378  gpgiedgdmellem  48537  lindslinindsimp1  48948  lindslinindimp2lem4  48952  lincresunit3  48972  iscnrm3llem1  49439