Theorem elpwid 3664

Description: An element of a power class is a subclass. Deduction form of elpwi 3662. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
elpwid.1	⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Assertion

Ref	Expression
elpwid	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Proof of Theorem elpwid

Step	Hyp	Ref	Expression
1		elpwid.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)
2		elpwi 3662	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2201   ⊆ wss 3199  𝒫 cpw 3653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-in 3205  df-ss 3212  df-pw 3655

This theorem is referenced by:  fopwdom  7027  ssenen  7042  fival  7174  fiuni  7182  3nelsucpw1  7457  elnp1st2nd  7701  ixxssxr  10140  elfzoelz  10387  restid2  13354  epttop  14843  neiss2  14895  blssm  15174  blin2  15185  cncfrss  15328  cncfrss2  15329  dvidsslem  15446  dvconstss  15451  plybss  15486  uhgrss  15955  upgrss  15979  upgr1een  16004  usgrss  16057  eupth2lemsfi  16358  pw1ndom3lem  16648  pwle2  16659