Theorem elpwd 4547

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114   ⊆ wss 3936  𝒫 cpw 4539

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  sselpwd  5230  pwel  5282  f1opw2  7400  pwuncl  7492  f1opwfi  8828  ackbij1lem6  9647  ackbij1lem11  9652  mreacs  16929  sylow3lem3  18754  sylow3lem6  18757  cmpcov  21997  tgqtop  22320  filss  22461  fnpreimac  30416  pcmplfin  31124  indval  31272  reprval  31881  scutval  33265  bj-sselpwuni  34346  bj-discrmoore  34406  dmvolss  42290  sge0xaddlem1  42735  meadjuni  42759  ovnval2b  42854  ovnsubadd2lem  42947  vonvolmbllem  42962  vonvolmbl  42963  smfresal  43083  smfpimbor1lem1  43093  sprsymrelfvlem  43672  lindslinindsimp1  44532  lindslinindimp2lem4  44536  lincresunit3  44556