Theorem elpwd 4548

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  sselpwd  5266  pwel  5319  frd  5582  f1opw2  7616  pwuncl  7718  naddunif  8623  f1opwfi  9260  ackbij1lem6  10140  ackbij1lem11  10145  indval  12156  mreacs  17618  sylow3lem3  19598  sylow3lem6  19601  cmpcov  23367  tgqtop  23690  filss  23831  nulsltsd  27786  nulsgtsd  27787  cutsval  27789  madecut  27892  cofcut1  27929  cutlt  27941  elons2d  28268  oncutlt  28273  bdayons  28285  fnpreimac  32761  exsslsb  33759  pcmplfin  34023  rspectopn  34030  zarclsint  34035  zarcmplem  34044  reprval  34773  bj-sselpwuni  37376  bj-discrmoore  37442  dmvolss  46434  sge0xaddlem1  46882  meadjuni  46906  ovnval2b  47001  ovnsubadd2lem  47094  vonvolmbllem  47109  vonvolmbl  47110  smfresal  47237  smfpimbor1lem1  47247  sprsymrelfvlem  47965  isubgruhgr  48359  grimuhgr  48378  gpgiedgdmellem  48537  lindslinindsimp1  48948  lindslinindimp2lem4  48952  lincresunit3  48972  iscnrm3llem1  49439