Theorem elpwd 4628

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-pw 4624

This theorem is referenced by:  sselpwd  5346  pwel  5399  frd  5656  f1opw2  7705  pwuncl  7805  naddunif  8749  f1opwfi  9426  ackbij1lem6  10293  ackbij1lem11  10298  mreacs  17716  sylow3lem3  19671  sylow3lem6  19674  cmpcov  23418  tgqtop  23741  filss  23882  scutval  27863  madecut  27939  cofcut1  27972  cutlt  27984  elons2d  28300  fnpreimac  32689  pcmplfin  33806  rspectopn  33813  zarclsint  33818  zarcmplem  33827  indval  33977  reprval  34587  bj-sselpwuni  37016  bj-discrmoore  37077  dmvolss  45906  sge0xaddlem1  46354  meadjuni  46378  ovnval2b  46473  ovnsubadd2lem  46566  vonvolmbllem  46581  vonvolmbl  46582  smfresal  46709  smfpimbor1lem1  46719  sprsymrelfvlem  47364  isubgruhgr  47738  grimuhgr  47762  lindslinindsimp1  48186  lindslinindimp2lem4  48190  lincresunit3  48210  iscnrm3llem1  48629