Theorem elpwd 4558

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113   ⊆ wss 3899  𝒫 cpw 4552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-pw 4554

This theorem is referenced by:  sselpwd  5271  pwel  5324  frd  5579  f1opw2  7611  pwuncl  7713  naddunif  8619  f1opwfi  9254  ackbij1lem6  10132  ackbij1lem11  10137  mreacs  17579  sylow3lem3  19556  sylow3lem6  19559  cmpcov  23331  tgqtop  23654  filss  23795  scutval  27768  madecut  27855  cofcut1  27891  cutlt  27903  elons2d  28227  onscutlt  28232  bdayon  28240  fnpreimac  32698  indval  32881  exsslsb  33702  pcmplfin  33966  rspectopn  33973  zarclsint  33978  zarcmplem  33987  reprval  34716  bj-sselpwuni  37194  bj-discrmoore  37255  dmvolss  46171  sge0xaddlem1  46619  meadjuni  46643  ovnval2b  46738  ovnsubadd2lem  46831  vonvolmbllem  46846  vonvolmbl  46847  smfresal  46974  smfpimbor1lem1  46984  sprsymrelfvlem  47678  isubgruhgr  48056  grimuhgr  48075  gpgiedgdmellem  48234  lindslinindsimp1  48645  lindslinindimp2lem4  48649  lincresunit3  48669  iscnrm3llem1  49136