Theorem elpwd 4468

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

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2083   ⊆ wss 3865  𝒫 cpw 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-in 3872  df-ss 3880  df-pw 4461

This theorem is referenced by:  sselpwd  5128  pwel  5243  f1opw2  7265  f1opwfi  8681  ackbij1lem6  9500  ackbij1lem11  9505  mreacs  16762  sylow3lem3  18488  sylow3lem6  18491  cmpcov  21685  tgqtop  22008  filss  22149  fnpreimac  30102  pcmplfin  30737  indval  30885  reprval  31494  scutval  32876  bj-discrmoore  34024  dmvolss  41834  sge0xaddlem1  42279  meadjuni  42303  ovnval2b  42398  ovnsubadd2lem  42491  vonvolmbllem  42506  vonvolmbl  42507  smfresal  42627  smfpimbor1lem1  42637  sprsymrelfvlem  43156  lindslinindsimp1  44014  lindslinindimp2lem4  44018  lincresunit3  44038