Theorem elpwd 4570

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146   ⊆ wss 3906  𝒫 cpw 4564

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-pw 4566

This theorem is used by:  pwidg  4584  sselpwd  5301  pwel  5354  frd  5620  f1opw2  7675  pwuncl  7775  naddunif  8686  f1opwfi  9320  ackbij1lem6  10223  ackbij1lem11  10228  indval  12236  mreacs  17736  sylow3lem3  19743  sylow3lem6  19746  cmpcov  23596  tgqtop  23920  filss  24061  nulsltsd  28021  nulsgtsd  28022  cutsval  28024  madecut  28127  cofcut1  28164  cutlt  28176  elons2d  28503  oncutlt  28508  bdayons  28520  fnpreimac  33086  exsslsb  34051  pcmplfin  34314  rspectopn  34321  zarclsint  34326  zarcmplem  34335  reprval  35062  bj-sselpwuni  37743  bj-discrmoore  37810  dmvolss  46757  sge0xaddlem1  47205  meadjuni  47229  ovnval2b  47324  ovnsubadd2lem  47417  vonvolmbllem  47432  vonvolmbl  47433  smfresal  47560  smfpimbor1lem1  47570  sprsymrelfvlem  48297  isubgruhgr  48691  grimuhgr  48710  gpgiedgdmellem  48869  lindslinindsimp1  49294  lindslinindimp2lem4  49298  lincresunit3  49318  iscnrm3llem1  49784