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 2733

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

This theorem is used by:  pwidg  4577  sselpwd  5290  pwel  5343  frd  5608  f1opw2  7674  pwuncl  7782  naddunif  8696  f1opwfi  9338  ackbij1lem6  10295  ackbij1lem11  10300  indval  12316  mreacs  17825  sylow3lem3  19836  sylow3lem6  19839  cmpcov  23700  tgqtop  24024  filss  24165  nulsltsd  28156  nulsgtsd  28157  cutsval  28159  madecut  28262  cofcut1  28299  cutlt  28311  elons2d  28638  oncutlt  28643  bdayons  28655  fnpreimac  33257  exsslsb  34222  pcmplfin  34485  rspectopn  34492  zarclsint  34497  zarcmplem  34506  reprval  35232  bj-sselpwuni  37945  bj-discrmoore  38012  dmvolss  46964  sge0xaddlem1  47412  meadjuni  47436  ovnval2b  47531  ovnsubadd2lem  47624  vonvolmbllem  47639  vonvolmbl  47640  smfresal  47767  smfpimbor1lem1  47777  sprsymrelfvlem  48541  isubgruhgr  48935  grimuhgr  48954  gpgiedgdmellem  49113  lindslinindsimp1  49538  lindslinindimp2lem4  49542  lincresunit3  49562  iscnrm3llem1  50026