Theorem elpwd 4581

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108   ⊆ wss 3926  𝒫 cpw 4575

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-pw 4577

This theorem is referenced by:  sselpwd  5298  pwel  5351  frd  5610  f1opw2  7662  pwuncl  7764  naddunif  8705  f1opwfi  9368  ackbij1lem6  10238  ackbij1lem11  10243  mreacs  17670  sylow3lem3  19610  sylow3lem6  19613  cmpcov  23327  tgqtop  23650  filss  23791  scutval  27764  madecut  27846  cofcut1  27880  cutlt  27892  elons2d  28212  onscutlt  28217  bdayon  28225  fnpreimac  32649  indval  32830  exsslsb  33636  pcmplfin  33891  rspectopn  33898  zarclsint  33903  zarcmplem  33912  reprval  34642  bj-sselpwuni  37068  bj-discrmoore  37129  dmvolss  46014  sge0xaddlem1  46462  meadjuni  46486  ovnval2b  46581  ovnsubadd2lem  46674  vonvolmbllem  46689  vonvolmbl  46690  smfresal  46817  smfpimbor1lem1  46827  sprsymrelfvlem  47504  isubgruhgr  47881  grimuhgr  47900  gpgiedgdmellem  48050  lindslinindsimp1  48433  lindslinindimp2lem4  48437  lincresunit3  48457  iscnrm3llem1  48923