Theorem elpwd 4566

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147   ⊆ wss 3900  𝒫 cpw 4560

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-pw 4562

This theorem is used by:  pwidg  4581  sselpwd  5297  pwel  5350  frd  5615  f1opw2  7708  pwuncl  7816  naddunif  8741  f1opwfi  9383  ackbij1lem6  10341  ackbij1lem11  10346  indval  12363  mreacs  17882  sylow3lem3  19894  sylow3lem6  19897  cmpcov  23762  tgqtop  24086  filss  24227  nulsltsd  28220  nulsgtsd  28221  cutsval  28223  madecut  28326  cofcut1  28363  cutlt  28375  elons2d  28702  oncutlt  28707  bdayons  28719  fnpreimac  33362  exsslsb  34340  cmpcref  34593  pcmplfin  34603  rspectopn  34610  zarclsint  34615  zarcmplem  34624  omssubadd  35043  reprval  35350  bj-sselpwuni  38235  bj-discrmoore  38302  ishfstruct  46295  dmvolss  47268  sge0xaddlem1  47716  meadjuni  47740  ovnval2b  47835  ovnsubadd2lem  47928  vonvolmbllem  47943  vonvolmbl  47944  smfresal  48071  smfpimbor1lem1  48081  sprsymrelfvlem  48845  isubgruhgr  49239  grimuhgr  49258  gpgiedgdmellem  49417  lindslinindsimp1  49900  lindslinindimp2lem4  49904  lincresunit3  49924  iscnrm3llem1  50394