Theorem elpwd 4573

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2149   ⊆ wss 3913  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-pw 4569

This theorem is referenced by:  pwidg  4587  sselpwd  5299  pwel  5353  frd  5619  f1opw2  7666  pwuncl  7768  naddunif  8679  f1opwfi  9312  ackbij1lem6  10206  ackbij1lem11  10211  indval  12220  mreacs  17713  sylow3lem3  19698  sylow3lem6  19701  cmpcov  23514  tgqtop  23837  filss  23978  nulsltsd  27935  nulsgtsd  27936  cutsval  27938  madecut  28041  cofcut1  28078  cutlt  28090  elons2d  28417  oncutlt  28422  bdayons  28434  fnpreimac  32955  exsslsb  33931  pcmplfin  34194  rspectopn  34201  zarclsint  34206  zarcmplem  34215  reprval  34941  bj-sselpwuni  37573  bj-discrmoore  37640  dmvolss  46590  sge0xaddlem1  47038  meadjuni  47062  ovnval2b  47157  ovnsubadd2lem  47250  vonvolmbllem  47265  vonvolmbl  47266  smfresal  47393  smfpimbor1lem1  47403  sprsymrelfvlem  48127  isubgruhgr  48521  grimuhgr  48540  gpgiedgdmellem  48699  lindslinindsimp1  49121  lindslinindimp2lem4  49125  lincresunit3  49145  iscnrm3llem1  49611