Theorem elpwd 4553

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2111   ⊆ wss 3897  𝒫 cpw 4547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-pw 4549

This theorem is referenced by:  sselpwd  5264  pwel  5317  frd  5571  f1opw2  7601  pwuncl  7703  naddunif  8608  f1opwfi  9240  ackbij1lem6  10115  ackbij1lem11  10120  mreacs  17564  sylow3lem3  19541  sylow3lem6  19544  cmpcov  23304  tgqtop  23627  filss  23768  scutval  27741  madecut  27828  cofcut1  27864  cutlt  27876  elons2d  28196  onscutlt  28201  bdayon  28209  fnpreimac  32653  indval  32834  exsslsb  33609  pcmplfin  33873  rspectopn  33880  zarclsint  33885  zarcmplem  33894  reprval  34623  bj-sselpwuni  37092  bj-discrmoore  37153  dmvolss  46031  sge0xaddlem1  46479  meadjuni  46503  ovnval2b  46598  ovnsubadd2lem  46691  vonvolmbllem  46706  vonvolmbl  46707  smfresal  46834  smfpimbor1lem1  46844  sprsymrelfvlem  47529  isubgruhgr  47907  grimuhgr  47926  gpgiedgdmellem  48085  lindslinindsimp1  48497  lindslinindimp2lem4  48501  lincresunit3  48521  iscnrm3llem1  48988