Theorem elpwd 4572

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109   ⊆ wss 3917  𝒫 cpw 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-pw 4568

This theorem is referenced by:  sselpwd  5286  pwel  5339  frd  5598  f1opw2  7647  pwuncl  7749  naddunif  8660  f1opwfi  9314  ackbij1lem6  10184  ackbij1lem11  10189  mreacs  17626  sylow3lem3  19566  sylow3lem6  19569  cmpcov  23283  tgqtop  23606  filss  23747  scutval  27719  madecut  27801  cofcut1  27835  cutlt  27847  elons2d  28167  onscutlt  28172  bdayon  28180  fnpreimac  32602  indval  32783  exsslsb  33599  pcmplfin  33857  rspectopn  33864  zarclsint  33869  zarcmplem  33878  reprval  34608  bj-sselpwuni  37045  bj-discrmoore  37106  dmvolss  45990  sge0xaddlem1  46438  meadjuni  46462  ovnval2b  46557  ovnsubadd2lem  46650  vonvolmbllem  46665  vonvolmbl  46666  smfresal  46793  smfpimbor1lem1  46803  sprsymrelfvlem  47495  isubgruhgr  47872  grimuhgr  47891  gpgiedgdmellem  48041  lindslinindsimp1  48450  lindslinindimp2lem4  48454  lincresunit3  48474  iscnrm3llem1  48941